-
Looking for winning strategies in two-player games on Petri nets with partial observability
Authors:
Federica Adobbati,
Luca Bernardinello,
Lucia Pomello
Abstract:
We define a game on 1-safe Petri nets, where a user plays against an environment in order to reach a goal on the system. The goal is expressed through an LTL-X formula, and represents a behaviour of the system that the user needs to guarantee. The user can try to reach his goal by controlling a subset of transitions, and by observing a subset of local states. Although we do not put any requirement…
▽ More
We define a game on 1-safe Petri nets, where a user plays against an environment in order to reach a goal on the system. The goal is expressed through an LTL-X formula, and represents a behaviour of the system that the user needs to guarantee. The user can try to reach his goal by controlling a subset of transitions, and by observing a subset of local states. Although we do not put any requirement on the local states observable by the user, we assume that he cannot be sure to observe them in the exact moment in which they become marked. For this reason, we define a notion of stability of the observation. We propose a method to determine whether the user has a winning strategy, i.e. if he can win every play by taking some decisions based on the information available for him.
△ Less
Submitted 4 April, 2022;
originally announced April 2022.
-
Asynchronous games on Petri nets and ATL
Authors:
Federica Adobbati,
Luca Bernardinello,
Lucia Pomello
Abstract:
We define a game on distributed Petri nets, where several players interact with each other, and with an environment. The players, or users, have perfect knowledge of the current state, and pursue a common goal. Such goal is expressed by Alternating-time Temporal Logic (ATL). The users have a winning strategy if they can cooperate to reach their goal, no matter how the environment behaves. We show…
▽ More
We define a game on distributed Petri nets, where several players interact with each other, and with an environment. The players, or users, have perfect knowledge of the current state, and pursue a common goal. Such goal is expressed by Alternating-time Temporal Logic (ATL). The users have a winning strategy if they can cooperate to reach their goal, no matter how the environment behaves. We show that such a game can be translated into a game on concurrent game structures (introduced in order to give a semantics to ATL). We compare our game with the game on concurrent game structures and discuss the differences between the two approaches. Finally, we show that, when we consider memoryless strategies and a fragment of ATL, we can construct a concurrent game structure from the Petri net, such that an ATL formula is verified on the net if, and only if, it is verified on the game structure.
△ Less
Submitted 14 July, 2021;
originally announced July 2021.
-
Soundness-preserving composition of synchronously and asynchronously interacting workflow net components
Authors:
Luca Bernardinello,
Irina Lomazova,
Roman Nesterov,
Lucia Pomello
Abstract:
In this paper, we propose a compositional approach to constructing correct formal models of information systems from correct models of interacting components. Component behavior is represented using workflow nets - a class of Petri nets. Interactions among components are encoded in an additional interface net. The proposed approach is used to model and compose synchronously and asynchronously inte…
▽ More
In this paper, we propose a compositional approach to constructing correct formal models of information systems from correct models of interacting components. Component behavior is represented using workflow nets - a class of Petri nets. Interactions among components are encoded in an additional interface net. The proposed approach is used to model and compose synchronously and asynchronously interacting workflow nets. Using Petri net morphisms and their properties, we prove that the composition of interacting workflow nets preserves the correctness of components and of an interface.
△ Less
Submitted 2 August, 2022; v1 submitted 15 January, 2020;
originally announced January 2020.
-
Compositional Discovery of Workflow Nets from Event Logs Using Morphisms
Authors:
Luca Bernardinello,
Irina Lomazova,
Roman Nesterov,
Lucia Pomello
Abstract:
This paper presents a modular approach to discover process models for multi-agent systems from event logs. System event logs are filtered according to individual agent behavior. We discover workflow nets for each agent using existing process discovery algorithms. We consider asynchronous interactions among agents. Given a specification of an interaction protocol, we propose a general scheme of wor…
▽ More
This paper presents a modular approach to discover process models for multi-agent systems from event logs. System event logs are filtered according to individual agent behavior. We discover workflow nets for each agent using existing process discovery algorithms. We consider asynchronous interactions among agents. Given a specification of an interaction protocol, we propose a general scheme of workflow net composition. By using morphisms, we prove that this composition preserves soundness of components. A quality evaluation shows the increase in the precision of models discovered by the proposed approach.
△ Less
Submitted 11 June, 2018;
originally announced June 2018.
-
Between quantum logic and concurrency
Authors:
Luca Bernardinello,
Carlo Ferigato,
Lucia Pomello
Abstract:
We start from two closure operators defined on the elements of a special kind of partially ordered sets, called causal nets. Causal nets are used to model histories of concurrent processes, recording occurrences of local states and of events. If every maximal chain (line) of such a partially ordered set meets every maximal antichain (cut), then the two closure operators coincide, and generate a…
▽ More
We start from two closure operators defined on the elements of a special kind of partially ordered sets, called causal nets. Causal nets are used to model histories of concurrent processes, recording occurrences of local states and of events. If every maximal chain (line) of such a partially ordered set meets every maximal antichain (cut), then the two closure operators coincide, and generate a complete orthomodular lattice. In this paper we recall that, for any closed set in this lattice, every line meets either it or its orthocomplement in the lattice, and show that to any line, a two-valued state on the lattice can be associated. Starting from this result, we delineate a logical language whose formulas are interpreted over closed sets of a causal net, where every line induces an assignment of truth values to formulas. The resulting logic is non-classical; we show that maximal antichains in a causal net are associated to Boolean (hence "classical") substructures of the overall quantum logic.
△ Less
Submitted 31 July, 2014;
originally announced August 2014.
-
Orthomodular Lattices Induced by the Concurrency Relation
Authors:
Luca Bernardinello,
Lucia Pomello,
Stefania Rombolà
Abstract:
We apply to locally finite partially ordered sets a construction which associates a complete lattice to a given poset; the elements of the lattice are the closed subsets of a closure operator, defined starting from the concurrency relation. We show that, if the partially ordered set satisfies a property of local density, i.e.: N-density, then the associated lattice is also orthomodular. We then…
▽ More
We apply to locally finite partially ordered sets a construction which associates a complete lattice to a given poset; the elements of the lattice are the closed subsets of a closure operator, defined starting from the concurrency relation. We show that, if the partially ordered set satisfies a property of local density, i.e.: N-density, then the associated lattice is also orthomodular. We then consider occurrence nets, introduced by C.A. Petri as models of concurrent computations, and define a family of subsets of the elements of an occurrence net; we call those subsets "causally closed" because they can be seen as subprocesses of the whole net which are, intuitively, closed with respect to the forward and backward local state changes. We show that, when the net is K-dense, the causally closed sets coincide with the closed sets induced by the closure operator defined starting from the concurrency relation. K-density is a property of partially ordered sets introduced by Petri, on the basis of former axiomatizations of special relativity theory.
△ Less
Submitted 12 November, 2009;
originally announced November 2009.
