Wyniki wyszukiwania - BazTech

1

The Complexity of Diagnosability and Opacity Verification for Petri Nets

Bérard B., Haar S., Schmitz S., Schwoon S.

Fundamenta Informaticae

|

2018

|

Vol. 161, nr 4

317--349

EN

Diagnosability and opacity are two well-studied problems in discrete-event systems. We revisit these two problems with respect to expressiveness and complexity issues. We first relate different notions of diagnosability and opacity. We consider in particular fairness issues and extend the definition of Germanos et al. [ACM TECS, 2015] of weakly fair diagnosability for safe Petri nets to general Petri nets and to opacity questions. Second, we provide a global picture of complexity results for the verification of diagnosability and opacity. We show that diagnosability is NL-complete for finite state systems, PSPACE-complete for safe convergent Petri nets (even with fairness), and EXPSPACE-complete for general Petri nets without fairness, while non diagnosability is inter-reducible with reachability when fault events are not weakly fair. Opacity is ESPACE-complete for safe Petri nets (even with fairness) and undecidable for general Petri nets already without fairness.

2

Closed Sets in Occurrence Nets with Conflicts

Bernardinello L., Ferigato C., Haar S., Pomello L.

Fundamenta Informaticae

|

2014

|

Vol. 133, nr 4

323--344

EN

The semantics of concurrent processes can be defined in terms of partially ordered sets. Occurrence nets, which belong to the family of Petri nets, model concurrent processes as partially ordered sets of occurrences of local states and local events. On the basis of the associated concurrency relation, a closure operator can be defined, giving rise to a lattice of closed sets. Extending previous results along this line, the present paper studies occurrence nets with forward conflicts, modelling families of processes. It is shown that the lattice of closed sets is orthomodular, and the relations between closed sets and some particular substructures of an occurrence net are studied. In particular, the paper deals with runs, modelling concurrent histories, and trails, corresponding to possible histories of sequential components. A second closure operator is then defined by means of an iterative procedure. The corresponding closed sets, here called ‘dynamically closed’, are shown to form a complete lattice, which in general is not orthocomplemented. Finally, it is shown that, if an occurrence net satisfies a property called B-density, which essentially says that any antichain meets any trail, then the two notions of closed set coincide, and they form a complete, algebraic orthomodular lattice.

3

Building Occurrence Nets from Reveals Relations

Balaguer S., Chatain T., Haar S.

Fundamenta Informaticae

|

2013

|

Vol. 123, nr 3

245--272

EN

Occurrence nets are a well known partial order model for the concurrent behavior of Petri nets. The causality and conflict relations between events, which are explicitly represented in occurrence nets, induce logical dependencies between event occurrences: the occurrence of an event e in a run implies that all its causal predecessors also occur, and that no event in conflict with e occurs. But these structural relations do not express all the logical dependencies between event occurrences in maximal runs: in particular, the occurrence of e in any maximal run may imply the occurrence of another event that is not a causal predecessor of e, in that run. The reveals relation has been introduced to express this dependency between two events. Here we generalize the reveals relation to express more general dependencies, involving more than two events, and we introduce ERL logic to express them as boolean formulas. Finally we answer the synthesis problem that arises : given an ERL formula φ, is there an occurrence net N such that φ describes exactly the dependencies between the events of N?

4

Probabilistic Cluster Unfoldings

Haar S.

Fundamenta Informaticae

|

2002

|

Vol. 53, nr 3,4

281-314

EN

This article introduces probabilistic cluster branching processes, a probabilistic unfolding semantics for untimed Petri nets with no structural or safety assumptions. The unfolding is constructed by local choices on each cluster (conflict closed subnet), while the authorization for cluster actions is governed by a stochastic trace, the policy. The probabilistic model for this semantics yields probability measures for concurrent runs. We introduce and characterize stopping times for this model, and prove a strong Markov property. Particularly adequate probability measures for the choice of step in a cluster, as well as for the policy, are obtained by constructing Markov Fields from suitable marking-dependent Gibbs potentials.

5

Clusters, Confusion and Unfoldings

Haar S.

Fundamenta Informaticae

|

2001

|

Vol. 47, nr 3,4

259-270

EN

We study independence of events in the unfoldings of Petri nets, in particular indirect influences between concurrent events: Confusion in the sense of Smith [11] and weak interference. The role of structural (conflict) clusters is investigated, and a new unfolding semantics based on clusters motivated and introduced.

6

Occurrence net logics

Haar S.

Fundamenta Informaticae

|

2000

|

Vol. 43, Nr 1-4

105-127

EN

This paper investigates Occurrence (Petri) Nets on two levels: their structural theory and their interpretation in branching unfolding semantics of Petri Net systems. The key issue is the decomposition of occurrence nets into substructures given by the node relations associated with causal ordering, concurrency, and conflict. In addition to lines and cuts, which have long been studied in the context of causal nets, we introduce and study branches, trails, choices, and alternatives. All finite systems will be shown to satisfy certain density properties, i.e. non-empty intersections of substructures as above. On the semantic level, we introduce partial order logics to be interpreted on two different kind of frames, given by substructures of occurrence nets: on the frame of cuts, the CTL* type logics BFC and BLC, and the ``non-branching'' logic LLC, taylored to the frame given by the lattice of choices.