Go beyond the SCOPE: A temporal situation calculus-based software tool for time Petri nets

Abstract

This paper presents a straightforward and mathematically rigorous software tool for Time Petri Nets (TPN). More precisely, we first build up a formal process ontology of TPNs by extending SCOPE (Situation Calculus Ontology for PEtri nets) with temporal constraints. We then demonstrate that, with this temporal SCOPE, sequential, iterative, or nondeterministic composite sequences of transition firings in TPNs can be further axiomatized through macro-expanding the basic action of transition firing. Finally, it is shown that theorem-proving, i.e., computing the consequences of such an ontology, can be carried out efficiently through logic programming in Prolog. Potential future applications of our approach are also discussed. © 2012 Springer-Verlag.