Building Occurrence Nets from Reveals Relations

• Autorzy: Balaguer, S. , Chatain, T. , Haar, S.
• Języki publikacji: EN

Abstrakty

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?

Słowa kluczowe

EN

synthesis of concurrent systems; occurrence nets; event logics; Petri nets; maximal runs

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2013
• Tom: Vol. 123, nr 3
• Strony: 245--272
• Opis fizyczny: Bibliogr. 27 poz., rys.

Twórcy

autor

Balaguer, S.

• INRIA & LSV (CNRS & ENS Cachan) 61, avenue du Pr´esident Wilson 94235 CACHAN Cedex, France,

autor

Chatain, T.

• INRIA & LSV (CNRS & ENS Cachan) 61, avenue du Pr´esident Wilson 94235 CACHAN Cedex, France,

autor

Haar, S.

• INRIA & LSV (CNRS & ENS Cachan) 61, avenue du Pr´esident Wilson 94235 CACHAN Cedex, France,

Bibliografia

• [1] Badouel, E., Caillaud, B., Darondeau, P.: Distributing Finite Automata through Petri Net Synthesis, Journal on Formal Aspects of Computing, 13, 2002, 447–470.
• [2] Badouel, E., Darondeau, P.: Theory of regions, in: Lectures on Petri Nets I: Basic Models, vol. 1491 of LNCS, Springer Berlin / Heidelberg, 1998, 529–586.
• [3] Balaguer, S., Chatain, T., Haar, S.: Building Tight Occurrence Nets from Reveals Relations, Proceedings of the 11th International Conference on Application of Concurrency to System Design (ACSD’11) (B. Caillaud, J. Carmona, Eds.), IEEE Computer Society Press, Newcastle upon Tyne, UK, June 2011.
• [4] Baldan, P., Corradini, A.,Montanari, U.: Contextual Petri Nets, Asymmetric Event Structures, and Processes, Information and Computation, 171(1), 2001, 1–49.
• [5] Bergenthum, R., Desel, J., Lorenz, R., Mauser, S.: Synthesis of Petri Nets from Finite Partial Languages, Fundam. Inform., 88(4), 2008, 437–468.
• [6] Bernardinello, L.: Synthesis of Net Systems, ICATPN, 691, Springer, 1993, ISBN 3-540-56863-8.
• [7] Busi, N., Pinna, G. M.: Non Sequential Semantics for Contextual P/T Nets, Application and Theory of Petri Nets, 1091, Springer, 1996.
• [8] Carmona, J., Cortadella, J., Kishinevsky, M., Kondratyev, A., Lavagno, L., Yakovlev, A.: A Symbolic Algorithm for the Synthesis of Bounded Petri Nets, in: ICATPN, vol. 5062 of LNCS, Springer-Verlag, 2008, 92–111.
• [9] Chatain, T., Fabre, .: Factorization Properties of Symbolic Unfoldings of Colored Petri Nets, Petri Nets, 6128, Springer, 2010, ISBN 978-3-642-13674-0.
• [10] Chatain, T., Jard, C.: Symbolic Diagnosis of Partially Observable Concurrent Systems, FORTE, 3235, 2004.
• [11] Darondeau, P.: Deriving Unbounded Petri Nets from Formal Languages, CONCUR, 1466, Springer, 1998, ISBN 3-540-64896-8.
• [12] Desel, J., Reisig, W.: The synthesis problem of Petri nets, Acta Inf., 33, 1996, 297–315, ISSN 0001-5903.
• [13] Ehrenfeucht, A., Rozenberg, G.: Partial (Set) 2-Structures. Parts I and II, Acta Inf., 27(4), 1989, 315–368.
• [14] Ehrig, H., Hoffmann, K., Padberg, J., Baldan, P., Heckel, R.: High-Level Net Processes, Formal and Natural Computing, 2300, Springer, 2002.
• [15] Engelfriet, J.: Branching Processes of Petri Nets, Acta Inf., 28(6), 1991, 575–591.
• [16] Esparza, J., R¨omer, S., Vogler, W.: An Improvement of McMillan’s Unfolding Algorithm, Formal Methods in System Design, 20(3), 2002, 285–310.
• [17] Gastin, P., Kuske, D.: Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces, Information and Computation, 208(7), 2010, 797–816.
• [18] Haar, S.: Types of Asynchronous Diagnosability and the Reveals-Relation in Occurrence Nets, IEEE Transactions on Automatic Control, 55(10), 2010, 2310–2320.
• [19] Khomenko, V.: Model Checking Based on Prefixes of Petri Net Unfoldings, Ph.D. Thesis, School of Computing Science, University of Newcastle upon Tyne, 2003.
• [20] Khomenko, V., Koutny, M., Yakovlev, A.: Detecting State Encoding Conflicts in STG Unfoldings Using SAT, Fundam. Inf., 62(2), 2004, 221–241, ISSN 0169-2968.
• [21] McMillan, K. L.: Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits, CAV, 663, Springer, 1992, ISBN 3-540-56496-9.
• [22] Merlin, P. M.: A study of the recoverability of computing systems, Ph.D. Thesis, University of California, Irvine, 1974.
• [23] Nielsen, M., Plotkin, G. D., Winskel, G.: Petri Nets, Event Structures and Domains, Part I, Theor. Comput. Sci., 13, 1981, 85–108.
• [24] Penczek, W.: Branching Time and Partial Order in Temporal Logics, Time and Logic: A Computational Approach, UCL Press, 1995.
• [25] Vogler,W.: Fairness and Partial Order Semantics, Inf. Process. Lett., 55(1), 1995, 33–39.
• [26] Vogler,W.: Partial order semantics and read arcs, Theoretical Computer Science, 286(1), 2002, 33–63.
• [27] Winkowski, J.: Processes of Contextual Nets and their Characteristics, Fundamenta Informaticae, 36(1), 1998.