Skip to main content
SpringerLink
Log in

MSO Logic and the Partial Order Semantics of Place/Transition-Nets

  • Conference paper
  • First Online:
Theoretical Aspects of Computing - ICTAC 2015 (ICTAC 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9399))

Included in the following conference series:

Abstract

In this work, we study the interplay between monadic second order logic and the partial order theory of bounded place/transition-nets. First, we show that the causal behavior of any bounded p / t-net can be compared with respect to inclusion with the set of partial orders specified by a given MSO sentence \(\varphi \). Subsequently, we address the synthesis of Petri nets from MSO specifications. More precisely, we show that given any MSO sentence \(\varphi \), one can automatically construct a bounded Petri net whose behaviour minimally includes the set of partial orders specified by \(\varphi \). Combining this synthesis result with the comparability results we study three problems in the realm of automated correction of faulty Petri nets, and show that these problems are decidable.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    A Petri net is pure if no transition consumes and produces a token at the same place.

  2. 2.

    In the execution semantics the fact that an event \(v_1\) is smaller than an event \(v_2\) indicates that \(v_2\) occurs after \(v_1\), but \(v_1\) need not be necessarily the cause of \(v_2\). If N is a net and p is a place that is a linear combination of places in N, then N and \(N\cup \{p\}\) have the same execution behavior. This is not true for the causal semantics.

  3. 3.

    A DAG has slicewidth c if it can be decomposed into a unit decomposition over \(\overrightarrow{{\varSigma }}(c,T)\).

References

  1. Avellaneda, F., Morin, R.: Checking partial-order properties of vector addition systems with states. In: Proceedings of ACSD 2013, pp. 100–109. IEEE (2013)

    Google Scholar 

  2. Badouel, E., Darondeau, P.: On the synthesis of general Petri nets. Technical Report PI-1061, IRISA (1996)

    Google Scholar 

  3. Badouel, E., Darondeau, P.: Theory of regions. In: Reisig, W., Rozenberg, G. (eds.) Lectures on Petri Nets I: Basic Models. LNCS, vol. 1491, pp. 529–586. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  4. Bauderon, M., Courcelle, B.: Graph expressions and graph rewritings. Math. Syst. Theor. 20(2–3), 83–127 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  5. Bergenthum, R., Desel, J., Lorenz, R., Mauser, S.: Synthesis of Petri nets from infinite partial languages. In: Proceedings of ACSD 2008, pp. 170–179. IEEE (2008)

    Google Scholar 

  6. Brandenburg, F.-J., Skodinis, K.: Finite graph automata for linear and boundary graph languages. Theor. Comput. Sci. 332(1–3), 199–232 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  7. Bruggink, H.S., König, B.: On the recognizability of arrow and graph languages. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) Graph Transformations. LNCS, vol. 5214, pp. 336–350. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  8. Büchi, J.R.: Weak second order arithmetic and finite automata. Z. Math. Logik Grundl. Math. 6, 66–92 (1960)

    Article  MathSciNet  MATH  Google Scholar 

  9. Courcelle, B.: The monadic second-order logic of graphs I. Recognizable sets of finite graphs. Inf. Comput. 85(1), 12–75 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  10. Darondeau, P.: Deriving unbounded Petri nets from formal languages. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR’98 Concurrency Theory. LNCS, vol. 1466, pp. 533–548. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  11. Darondeau, P.: Region based synthesis of P/T-nets and its potential applications. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, p. 16. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  12. de Oliveira Oliveira, M.: Hasse diagram generators and Petri nets. Fundam. Inf. 105(3), 263–289 (2010)

    MathSciNet  MATH  Google Scholar 

  13. de Oliveira Oliveira, M.: Canonizable partial order generators. In: Dediu, A.-H., Martín-Vide, C. (eds.) LATA 2012. LNCS, vol. 7183, pp. 445–457. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  14. de Oliveira Oliveira, M.: Subgraphs satisfying MSO properties on z-topologically orderable digraphs. In: Gutin, G., Szeider, S. (eds.) IPEC 2013. LNCS, vol. 8246, pp. 123–136. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  15. Elgot, C.C.: Decision problems of finite automata and related arithmetics. Trans. Am. Math. Soc. 98, 21–52 (1961)

    Article  MathSciNet  MATH  Google Scholar 

  16. Engelfriet, J., et al.: Context-free graph grammars and concatenation of graphs. Acta Inf. 34, 773–803 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  17. Goltz, U., Reisig, W.: Processes of place/transition-nets. In: Diaz, J. (ed.) Automata, Languages and Programming. LNCS, vol. 154, pp. 264–277. Springer, Heidelberg (1983)

    Chapter  Google Scholar 

  18. Madhusudan, P., Thiagarajan, P.S.: Distributed controller synthesis for local specifications. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, p. 396. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  19. Petri, C.A.: Fundamentals of a theory of asynchronous information flow. Proc. of IFIP Congr. 62, 166–168 (1962). Munchen

    Google Scholar 

  20. Place, T., Zeitoun, M.: Separating regular languages with first-order logic. In: Proceedings of CSL/LICS, p. 75. ACM (2014)

    Google Scholar 

  21. Thomas, W.: Finite-state recognizability of graph properties. Theor. des Automates et Appl. 172, 147159 (1992)

    Google Scholar 

  22. Thomas, W.: Languages, automata, and logic. Handb. Formal Lang. Theor. 3, 389–455 (1997)

    Article  MathSciNet  Google Scholar 

  23. Vogler, Walter (ed.): Modular Construction and Partial Order Semantics of Petri Nets. LNCS, vol. 625. Springer, Heidelberg (1992)

    MATH  Google Scholar 

  24. von Essen, C., Jobstmann, B.: Program repair without regret. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 896–911. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

Download references

Acknowledgements

The author gratefully acknowledges financial support from the European Research Council, ERC grant agreement 339691, within the context of the project Feasibility, Logic and Randomness (FEALORA).

Author information

Authors and Affiliations

  1. Institute of Mathematics, Academy of Sciences of the Czech Republic, Prague, Czech Republic

    Mateus de Oliveira Oliveira

Authors
  1. Mateus de Oliveira Oliveira
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mateus de Oliveira Oliveira .

Editor information

Editors and Affiliations

  1. University of Lübeck, Lübeck, Schleswig-Holstein, Germany

    Martin Leucker

  2. Pontificia Universidad Javeriana-Cali, Cali, Colombia

    Camilo Rueda

  3. Pontificia Universidad Javeriana-Cali, CNRS LIX École Polytechnique de Paris, Palaiseau Cedex, France

    Frank D. Valencia

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

de Oliveira Oliveira, M. (2015). MSO Logic and the Partial Order Semantics of Place/Transition-Nets. In: Leucker, M., Rueda, C., Valencia, F. (eds) Theoretical Aspects of Computing - ICTAC 2015. ICTAC 2015. Lecture Notes in Computer Science(), vol 9399. Springer, Cham. https://doi.org/10.1007/978-3-319-25150-9_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-25150-9_22

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-25149-3

  • Online ISBN: 978-3-319-25150-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation