Automated Interpretation of S-Invariants of Predicate/Transition Nets: AnApplication of Non-Classical Logics

摘要

As an application of non-classical logics the interpretation of S-invariants ofpredicate/-transition nets is automated. The intention is to provide system designers with facilities for interpreting these invariants automatically. The idea is to prove compound logical consequences of two finite sets of premises derived from a given predicate/transition net model: a set of global premises consisting of formulae constructed from the S-invariants of the net and axioms of an equality theory associated with the net, and a set of local premises consisting of formulae representing the initial marking of the net. Construction of these premises is performed in three main steps. In the first step two algorithms for performing the transformations from two disjoint classes of S-invariants of the net into the formulae of first order modal logic are given. A finite axiomatization of a suitable equality theory associated with the net and, a set of literals representing the initial marking of the net are given in the second and third steps, respectively. A simplified proof method obtained by performing a number of simplifications to a more general already existing method is given next. It is employed for proving compound logical consequences of these two sets of premises within an adequate calculus of first order modal logic. A theorem stating the unprovability of formulae expressing progress properties and two representative examples illustrating the discussions for both classes of S-invariants close the paper.