For the most recent entries see the Petri Nets Newsletter.

Decidability results for the propositional fluent calculus.

Lehmann, H.; Leuschel, M.

In: Lecture Notes in Artificial Intelligence, Vol. 1861: Computational Logic, Proceedings of CL 2000, pages 762-776. Springer-Verlag, 2000.

Abstract: The paper investigates a small fragment, FCPL, of the fluent calculus. FCPL can be derived from the fluent calculus by allowing a domain description to contain a finite number of actions and fluents, only. Consequently, it is just powerful enough for specifying certain resource sensitive actions. This paper contributes to the research about the fluent calculus by (i) proving that even in this small fragment the entailment problem for a fairly restricted class of formulas is undecidable, (ii) showing decidability of a class of formulas which has interesting applications in resource planning. These results are achieved by establishing a tight correspondence between models of FCPL-theories and Petri nets. Then, many problems concerning FCPL-theories can be reduced to problems of the well developed Petri net theory. As a consequence of the correspondence on the structural level, strong relationship are expected between more general fluent calculus fragments and more general net classes, e.g., colored Petri nets or predicate/transition systems.

Keywords: Petri nets, decidability results, model checking, propositional fluent calculus, temporal logics.


Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography