Integrate Action Formalisms into Linear Temporal Description Logics

Franz BaaderFranz Baader, Hongkai LiuHongkai Liu, Anees ul MehdiAnees ul Mehdi

Download

Franz Baader, Hongkai Liu, Anees ul Mehdi
Integrate Action Formalisms into Linear Temporal Description Logics
Technical Report, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, volume LTCS-09-03, 2009. LTCS-Report

Details
Bibtex

KurzfassungAbstract
The verification problem for action logic programs with non-terminating behaviour is in general undecidable. In this paper, we consider a restricted setting in which the problem becomes decidable. On the one hand, we abstract from the actual execution sequences of a non-terminating program by considering infinite sequences of actions defined by a B"uchi automaton. On the other hand, we assume that the logic underlying our action formalism is a decidable description logic rather than full first-order predicate logic.
Bemerkung: Note: See http://lat.inf.tu-dresden.de/research/reports.html.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@techreport{ BMLSW-LTCS-09-03,
  address = {Germany},
  author = {Franz {Baader} and Hongkai {Liu} and Anees ul {Mehdi}},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-09-03},
  title = {{I}ntegrate {A}ction {F}ormalisms into {L}inear {T}emporal {D}escription {L}ogics},
  type = {LTCS-Report},
  year = {2009},
}