Abstract
We propose decision procedures based on regions for two problems on pure unbounded Petri nets with injective labelling. One problem is to construct nets from incomplete specifications, given by pairs of regular languages that impose respectively upper and lower bounds on the expected behaviours. The second problem is to derive equivalent nets from deterministic pushdown automata, thus exhibiting their hidden concurrency.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Autebert, J.M., Berstel, J., and Boasson, L., Context-Free Languages and Pushdown Automata. In vol. 1 of “Handbook of Formal Languages”, G. Rozenberg and A. Salomaa eds., Springer-Verlag (1997) 111–174
Badouel, E., Bernardinello, L. and Darondeau, Ph., Polynomial algorithms for the synthesis of bounded nets, Proceedings Caap 95, Lecture Notes in Computer Science 915 (1995) 647–679.
Badouel, E. and Darondeau, Ph., On the Synthesis of General Petri Nets, Inria Research Report no 3025 (1996).
Bernardinello, L., De Michelis, G., Petruni, K., and Vigna, S., On the Synchronic Structure of Transitions Systems. In “Structures in Concurrency Theory”, J. Desel ed., Springer-Verlag (1996) 11–31.
Bouajjani, A., and Habermehl, P., Constrained Properties, Semilinear Systems, and Petri Nets. Proceedings Concur 95, Lecture Notes in Computer Science 1119 (1995) 481–497.
Caillaud, B., Synet: un outil de synthèse de réseaux de Petri bornés, applications Inria Research Report no 3155 (1997).
Cortadella, J., Kishinevsky, M., Lavagno, L., and Yakovlev, A., Synthesizing Petri Nets from State-Based Models. Proceedings of ICCAD'95 (1995) 164–171.
Desel, J., and Reisig, W., The Synthesis Problem of Petri Nets. Acta Informatica, vol. 33 (1996) 297–315.
Droste, M., and Shortt, R.M., Bounded Petri Nets of Finite Dimension Have Only Finitely Many Reachable Markings. EATCS Bulletin No.48 (1992) 172–175.
Droste, M., and Shortt, R.M., Petri Nets and Automata with Concurrency Relations — an Adjunction, in ”Semantics of Programming Languages and Model Theory”, M. Droste and Y. Gurevich eds(1993) 69–87.
Ehrenfeucht, A., and Rozenberg, G., Partial (Set) 2-Structures; Part I: Basic Notions and the Representation Problem. Acta Informatica, vol. 27 (1990) 315–342.
Ehrenfeucht, A., and Rozenberg, G., Partial (Set) 2-Structures; Part II: State Spaces of Concurrent Systems. Acta Informatica, vol. 27 (1990) 343–368.
Harrisson, M.A., Introduction to Formal Language Theory. Addison-Wesley (1978).
Jancar, P., and Moller, F., Checking Regular Properties of Petri Nets, Proceedings Concur 95, Lecture Notes in Computer Science 962 (1995) 348–362.
Mukund, M., Petri Nets and Step Transition Systems. International Journal of Foundations of Computer Science, vol. 3 no. 4 (1992) 443–478.
Mauw, S. and Reniers, M.A., High-level Message Sequence Charts. Proceedings of the Eighth SDL Forum, North-Holland (1997).
Rackoff, C., The Covering and Boundedness Problems for Vector Addition Systems. Theoretical Computer Science, vol. 6 (1978) 223–231.
Rosier, L.E., and Yen, H.C., A Multiparameter Analysis of the Boundedness Problem for Vector Addition Systems. Journal of Computer and System Science, vol. 32 (1986) 105–135.
Schrijver, A., Theory of Linear and Integer Programming. John Wiley (1986).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Darondeau, P. (1998). Deriving unbounded Petri nets from formal languages. In: Sangiorgi, D., de Simone, R. (eds) CONCUR'98 Concurrency Theory. CONCUR 1998. Lecture Notes in Computer Science, vol 1466. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055646
Download citation
DOI: https://doi.org/10.1007/BFb0055646
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64896-3
Online ISBN: 978-3-540-68455-8
eBook Packages: Springer Book Archive