Integrate Action Formalisms into Linear Temporal Description Logics
Institut für Theoretische Informatik TU Dresden, Franz Baader, Anees ul Mehdi, Institut für Theoretische Informatik TU Dresden, Hongkai Liu, Institut für Theoretische Informatik TU Dresden · 2009
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üchi 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.