We report our preliminary results in implementing a tool to simulate and analyze Petri Nets and Elementary Object Systems from nets-within-net using the temporal ASP solver Telingo. Petri Nets (PNs) are a standard model of concurrent computation, introduced by Adam Petri in 1962 as a generalization of Finite State Automa1t]a.A[ t their barebones, they consist of a finite number of places hosting black tokens and a finite set of transitions that remove, add, and move the tokens on the places. Nowadays, several generalizations of PNs are available, which introduce additional features interesting for modeling. These range from simple inhibitory rules for the transitio2n]s t[o sophisticated tokens carrying data items or additional structures. A notable example are nets-within-nets, a paradigm in which tokens can in turn carry a full-fledged PN, possibly obtaining several levels of nesti3n]g. T[he simplest type of nets-within-nets are arguably Elementary Object Systems (EOSs), where the nesting is restricted to only two levels. Even if relatively simple, EOSs are appealing for modeling complex scenarios and multi-agent systems (MAS). In fact, the tokens at the higher level naturally represent agents, with their own internal state represented by the carried PN.
Clingo are [9] and [10]. However, none of them takes lossy PNs and EOSs in consideration and does
CEUR
ceur-ws.org not experiment with the temporal features of Telingo. In fact, the most appealing feature of Telingo is its support in constraints of Temporal Equilibrium Logic over finite traceTsE(L ) formulas, which we expect to be an excellent tool to flexibly control the amount of lossiness in the simulated runs.
2.1. EOSs A PN (see [11]) is a tuple = ( , , ) where is a finite place set, is a finite transition set (disjoint from ), and ∶ ( × ) ∪ ( × ) ⟶ ℕ is a flow function. Where useful, we equivalently interpre t via the functionspre ∶ → ( → ℕ) where pre ()() = (, ) and post ∶ → ( → ℕ) where post ()() = (, ) . PN configurations are called markings, i.e., (finite) multisets ∶ ⟶ ℕ
of places. We denote markings in set notation betwe{e{nand }}, possibly by prefixing the places with their multiplicity.
Example 1. Fig. 1 depicts the PN({ 0, 1, 2}, { 1}, ) where ( 0, 1) = (1, 1 ) = ( 1, 2) = 1 and ( 1, 0) = ( 1, 1) = (
2, 1), with initial marking0 = {{2 0, 5 1}}. The net reaches 1 = {{3 0, 2 2}}, covers 2 = {{}}, reaches a deadlock after two steps, and is not1-safe.
An EOS (see [12]) is, intuitively, asystem PN =̂ ⟨ , ̂ , ̂ ⟩̂ , whose tokens carry an internal PN taken from a fixed finite set of disjointobject PNs = ( , , ). contains the special object ■ = (∅, ∅, ∅). Each system net place can hold a single type of object net, according to a typing function ∶ ⟶̂ . EOSs fire events ⟨ ,̂ ⟩ , where ̂∈ ̂ and maps each ∈ to a multiset of transitions of itself. We denote b y( )
the sum of all∈ supp() such tha t ∈ , counting multiplicities. EOS tokens are nested, i.e., each token at a system pla∈ĉe ̂ carries a PN marking for the object ne t() . Such a token is denoted by⟨, ⟩̂ . The nested token is graphically represented by connecting, via a dashed line, ̂ with a representation o(f)
marked by . EOS markings, also called nested markings, are finite multisets of nested tokens. With a slight abuse of notation, we denote markings omitting double curly brackets from multiset notation and, if needed, concatenate tokens+u.sing Example 2. Fig. 2 depicts the system ne t ̂ (the idle transitions are omitted) and object net drone of an EOS = ⟨ , ̂ , , Θ⟩
modeling a drone that(
Technicall=y, {drone, ■ } (even if ■
is unused), ( base) = ( field) = drone, and Θ synchronizes takeOff and land (respectivelycharge) in ̂ with move (charge1 and charge2) in drone. Formally,Θ = {⟨takeOff, {{move}}⟩, ⟨land, {{move}}⟩, ⟨charge, {{charge1}}⟩, ⟨charge, {{charge2}}⟩}. The marking = ⟨drone, {{batt1, batt1}}⟩ represents a single partially charged dronebaatse, with two charge units in the first battery. ≤ if it is possible to injectively map each nested tok⟨e, n⟩̂ of to a nested token⟨, ̂ ′⟩ of
Given two markings and , we say: ≤ if contains more tokens than at the system level; where ≤ ′; finally, ≤ if there is some ′ such tha t≤ ′ ≤ or, equivalentl y≤ ′ ≤ . Given a nested marking , Π1() is the PN marking for the system net obtained by retaining only the system net tokens. Given also an object n e∈t , Π2 () is the PN marking for the object obtained by merging all markings carried by tokens at pla cesof type() = .
When an event = ⟨ ,̂ ⟩ ifres, ̂ consumes nested tokens at the system level in the standard way. For each object net, the carried markings of the consumed tokens are merged and the transitio nasrienfired, obtaining PN markings for each ∈ . Nested tokens with empty carried markings are produced at the system level according to the post-conditions.̂oFfinally, the marking s are non-deterministically distributed on the new nested marking, according to the typing function. This process can happen only if is enabled on under a mode (, ) , i.e., a pair of nested markings. This happens if ≤ , Π1() = pre( )̂ , Π2 () ≥ pre (( )) , Π1() = post( )̂ , and Π2 () = Π 2 () − pre (( )) + post (( )) , for each ∈ .
Telingo specializes the ASP solver Clingo to temporal domains and uses a logic program to specify ifnite runs. The program can use the scopes: initial,dynamic,always,final , which are evaluated at the first, each except first, each, and last step, respectively. Rule bodies can refer to the extension of the previous configuration by prefixing the literals with a prime. Finite-, linear-time formulas can appear in the dedicated atom&tel in constraints and behind default negation. For example, the constraint:- &tel{>?(a>a)} filters out all runs that eventually rea>c?hs(tands for eventually reach) a configuration with successor ′ (> stands for next) wherea is true on both. Telingo can be called setting the option--imax to a number of maximal step to be simulated. In the standard configuration, Telingo stops as soon as it finds a finite run satisfying the program or exceeds--imax.
The standard syntax for PNs is the PNML languag1e3][. For example, the input PNs provided by the MCC [14] are provided in PNML syntax. The first task we faced was the translation of PNML files into Logic Program (LP) files for Telingo. This required to fix a syntax to specify PNs in LP. Inspired by previous works (see, e.g., [10, 9]), we used the following solutions: • The number of places and of transitions are specified by two constants via the directives #const numPlaces=n and #const numPlaces=m. The names of the places and transition is abstracted away, i.e., they range {i0n, … , − 1} and {0, … , − 1} respectively. • Each pre-condition (, ) = and post-condition (, ) = is explicitly specified only if > 0 using the factpre(p,t,n) and post(p,t,n), respectively. These facts must be available during the whole computation and, thus, are put in the scope of #tphreogram always directive. • The file contains also the specification of the initial marking, which is represented as a function from places to numbers. Specifically, for each plac e hosting ∈ ℕ tokens (possibly = 0 ), we add the factmark(p,n) to the scope of the#program initial directive. Finally, we clean the Telingo output using the directiv#eshow mark/2. 1 #program always. 2 #const numPlaces=3. 3 #const numTransitions=1.
Example 3. The LP specification of the PN in Ex. 1 is:
4 pre(
8 mark(0,2).
9 mark(
Using ANTLR [15], we built an open source tool1[6], implemented in C++, to produce LP specifications out of MCC benchmarks.
The PN dynamics can be easily implemented in Telingo using the standard guess-and-check methodology of ASP: at each step, we1) sample a transition using a choice rul2e), check whether it is enabled on the previous marking using a constraint, an3d) deduce the facts encoding the new marking using a couple of simple rules that take in consideration the sampled transition, its conditions, and the previous marking. This last step is done using the rules 1 mark(P,K-N+M) :- pre(P,T,N), post(P,T,M),
'mark(P,K), fire(T). 2 mark(P,K+M) :- not pre(P,T,_), post(P,T,M),
'mark(P,K), fire(T).
The lossy dynamics is supported by allowing Telingo to possibly sample, next to the transitions at phase 1, also thelossy flag and, consequently, a sub-marking by firing the choice rule 3 mark(P,K-N) :- pre(P,T,N), not post(P,T,_),
'mark(P,K), fire(T). 4 mark(P,K) :- not pre(P,T,_), not post(P,T,_), 'mark(P,K), fire(T). 1 {mark(P,1..N)}=1 :- 'mark(P,N),lossy.
Assuming that the dynamics is encoded indynamic.lp, the simulation of the runs of maximum length of a PN encoded in pn.lp can be executed as follows: 1 Telingo dynamic.lp pn.lp 0 --imax=n
We considered several problems from the MCC. Since Telingo does not natively support branching
time formulas, we focused on linear paths namely reachability/coverability, deadlock detection, and
1-safeness. Since Telingo simulates runs incrementally, it is suficient to check these properties just at
the last step of the finite run. In fact, reachability/coverability and deadlock detection are all eventuality
properties. Moreover, also the opposite o1f-safeness, i.e., whether a non1--safe marking can be reached,
is of the same type.
1 #program final.
2 :- not mark(
Coverability can be similarly be specified using the rules 3 :- mark(1,N), N<0.
4 :- mark(2,N), N<2.
Example 4. To check the reachability in Ex1. of the marking(
4 :- not mark(2,2). 1 #program final. 2 :- mark(1,N), N<1.
Deadlock reachability requires to check the enabledness of all transitions and, so, requires their enumeration in a dedicated predicate. 1 #program final. 2 transition(0..numTransitions-1). 3 disabled(T) :- transition(T), pre(P,T,N),
mark(P,M), M<N.
Finally, (the opposite of1)-safeness is specified by
By adding these rules, if no maximum number of steps is signaled, Telingo will return a finite run witnessing the property, if it exists, or will never terminate, otherwi se.iIsfprovided, Telingo will always terminate, but will return a witnessing run of at moststeps.
For all these properties, we can seamlessly restrict the analysis to runs with atℓ ∈mℕost∪ {|ℕ|} many lossy-steps for anyℓ ∈ ℕ. For example, the rules problem deadlock deadlock 1-safeness 1-safeness lossiness none any none any
–imax =5 (s) UNSAT in 0.052
SAT in 0.009 UNSAT in 0.010 UNSAT in 0.013 –imax =10 (s) SAT in 0.622
SAT in 0.010 UNSAT in 0.014 UNSAT in 0.018 –imax =20 (s) SAT in 82.754
SAT in 0.009 UNSAT in 0.027 UNSAT in 0.032
tapaal (s) SAT in 5 − 6
NA UNSAT in 0
NA 1 #program initial.
iflter out all runs with at least two distinct lossy steps, so as to output only solutions witnessing the existence of suitable runs with at moℓs=t 1 lossy step. The parameteℓr can be controlled by nesting the string>(>? lossy) appropriately.
In the running example above, we used a simple PN to illustrate the concepts. However, for our experimentation, we considered several standard benchmarks taken from MC1C4][
which range across various industrial case studies and have diferent sizes of the PNs. We experimented with the analysis of deadlock reachability 1a-nsadfeness, for various maximal numbers of steps (5, 10, and 20): these properties can be expressed without any expert knowledge on the PN structure. We compared the output of our prototype for all benchmarks with the output provided, on the same instances, by the state-of-the-art taopoalal 3.9.3 [17]. The outputs match exactly; an indication of the correctness of the results, thereby giving our prototype a tool confidence10o0f% (despite noncompetitive times). We analyzed the benchmarks for both runs without lossy steps and with arbitrarily many lossy steps. A subset of our results and comparisons (for no loss) on a single PN is reported in Tab.1.
As for PNs, we started by fixing a syntax for EOS in LP. The major diference with PNs is the presence
of events and of nested tokens. Event⟨s,̂ ⟩ are specified by a name in a predicate event/1, a mapping
of the name t o in a predicateeventSys/2, and a mapping of the name to each transition inwith
multiplicity in a predicateeventObj/3
Example 5. The event takingOff = ⟨takeOff, {{move}}⟩ in Ex. 2 is specified by the facts
(
We came up with two encoding of nested markings. The first aims at representing nested tokens directly by linearizing the carried marking in a tuple. This requires to provide an order among the places and the usage of functional symbols as well as external Python functions.
Example 6. 2 nested tokens⟨base, {{2batt1}}⟩ for the EOS in Ex. 2 are specified by the fact nM(2, base, (2, 0)) assuming the orderbatt1 ≤ batt2 for the object netdrone.
The second representation employs a purely relational representation of each token in a relation tok/3. It keeps track of a token id, the token place, and the parent token (i.e., the token at the system level carrying it), if it exists (otherwise, a dummy const_asnyts is put in its place). The choice of identifiers is irrelevant as long as they form a primary key fotrok.
Example 7. One nested token from Ex.5 is equivalently captured by the fac(t1)s tok(0, base, _sys), (2) tok(1, batt1, 0), and (3) tok(2, batt1, 1).
When compared to PNs, EOS dynamics has to take care of two main aspects: the choice of enabling modes (, ) next to events, and the manipulation of nested markings. While modes range, in principle, over an infinite domain, we can restrict the choice over a finite set, by recalling th atshould be a sub-marking of the current marking. After choosing a and checking its compatibility with the enabling predicate for , the PN markingsΠ1() and Π2 () are univocally determined, for each object ne∈t . To materialize these projection in a nested markin,gwe make use of the relational representation of tokens. This allows us to easily assign children tokens to their parents non-deterministically. Afterwards, we convert in the nested token representation and update the marking. This solution requires the call of external Python functions handle the tuples for internal markings. The preliminary simulations on the EOS in Ex.2 were not optimal. We are currently working on a better implementation.
We specify EOS properties analogously to Sec3..3, but taking into account nested tokens. For example, the reachability of the targ⟨ebtase, {{batt1, batt1}}⟩ is checked by the rules 3 :- nM(N,base,Tup), Tup != (2,0).
4 :- nM(N,field,Tup). 1 #program final. 2 :- not nM(1,base,(2,0)).
Its coverability at the system net level is specified by rules 1 and 2 above. Coverability at the object level is specified by the rules 2 covered :- nM(1,base,Tup), Tup <= (2,0). 3 :- not covered. 2 covered :- nM(N,base,Tup), Tup <= (2,0).
3 :- not covered.
Even in this case, the specification of the amount of lossiness is orthogonal to that of the verification property and is performed using the same constraints as shown in Se3c..3.
We explored the applicability of Telingo to the simulation and analysis of lossy PNs and EOSs. Our approach is similar to1[0, 9], but we additionally encoded lossiness, EOSs, and provided a translator from PNML to LP syntax. We also conducted preliminary tests on the verification of deadlock reachability and 1-safeness of lossy PNs on runs with zero or arbitrarily many lossy steps. When compared with state-of-the-art tools ltikaepaal, we obtained sound results, yet with optimizable performances. On the one hand, the specification of lossy runs was especially elegant and flexible in Telingo, e.g., when compared to SMT-based PN verifiers [ 18]. Our approach addresses PNs in general and is applicable to PNs with reset, transfer, and inhibitory arcs. On the other hatnadp,aal does not natively support the analysis of properties under lossiness, unless somehow encoded in the PN itself. As a byproduct of our experiments, we provide a standalone utilit1y6][ compatible with Linux to translate standard PNML files to the PN LP syntax. We hope that this translator will provide ASP practitioners with a convenient tool to approach PN benchmarks. The prototype for EOS needs further development before tests can be meaningfully conducted. This task is challenging, since PN reachability is non-elementary and several reachability problems for lossy EOSs are undecidable in gener1a9l].[However, to the best of our knowledge, there are no available tools dedicated to lossy EOSs. [2] C. Dufourd, et al., Reset nets between decidability and undecidability, in: ICALP, volume 1443 of
LNCS, Springer, 1998, pp. 103–115. [3] R. Valk, Object Petri nets: Using the nets-within-nets paradigm, in: APN, volume 309L8NoCfS, 2003, pp. 819–848. [4] M. Köhler-Bussmeier, L. Capra, Robustness: A natural definition based on nets-within-nets, in:
PNSE, 2023. [5] F. Huch, Verification of Erlang programs using abstract interpretation and model checking, Ph.D.
thesis, RWTH Aachen, 2001. [6] A. Bouajjani, R. Mayr, Model checking lossy vector addition systems, in: STACS, ’99. [7] P. Cabalar, Temporal ASP: from logical foundations to practical use with telingo, in: Reasoning
Web. Declarative Artificial Intelligence, volume 13100 LoNfCS, 2021, pp. 94–114. [8] M. Gebser, et al., Multi-shot ASP solving with clingo, Theory Pract. Log. Program. 19 (2019) 27–82. [9] S. Anwar, et al., Encoding higher level extensions of Petri nets in answer set programming, in:
LPNMR, volume 8148 ofLNCS, 2013, pp. 116–121. [10] Y. Dimopoulos, et al., Encoding reversing Petri nets in answer set programming, in: RC, volume 12227 of LNCS, 2020, pp. 264–271. [11] T. Murata, Petri nets: Properties, analysis and applications, IEEE 77 (1989) 541–580. [12] M. Köhler-Bußmeier, A survey of decidability results for elementary object systems, Fundamenta
Informaticae 130 (2014) 99–123. [13] L. Hillah, et al., Extending pnml scope: A framework to combine Petri nets types, TOPNOC 6 (2012) 46–70. [14] F. Kordon, et al., Complete Results for the Model Checking Contest, https://mcc.lip6.fr/2023/results.php, 2023. [15] T. J. Parr, R. W. Quong, ANTLR: A predicated- LL(k) parser generator, Softw. Pract. Exp. 25 (1995) 789–810. [16] T. Prince, F. Di Cosmo, Nets within nets Telingo analyser, 2024. URhLt:tps://doi.org/10.5281/ zenodo.11401876. [17] J. F. Jensen, et al., TAPAAL and reachability analysis of P/T nets, TOPNOC 11 (2016) 307–318. [18] T. Prince, DCModelChecker 2.0: A BMC tool for Unbounded PN, 2022. URLh:ttps://doi.org/10.
5281/zenodo.7352391. [19] F. Di Cosmo, et al., Deciding reachability and coverability in lossy EOS, in: PNSE, 2024. To appear.