Advertisement

Concurrent Implementation of Asynchronous Transition Systems

  • Walter Vogler
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1639)

Abstract

The synthesis problem is to decide for a deterministic transition system whether a Petri net with an isomorphic reachability graph exists and in case to find such a net (which must have the arc-labels of the transition system as transitions). In this paper, we weaken isomorphism to some form of bisimilarity that also takes concurrency into account and we consider safe nets that may have additional internal transitions. To speak of concurrency, the transition system is enriched by an independence relation to an asynchronous transition system. For an arbitrary asynchronous transition system, we construct an ST-bisimilar net. We show how to decide effectively whether there exists a bisimilar net without internal transitions, in which case we can also find a history-preserving bisimilar net without internal transitions. Finally, we present a construction that inserts a new internal event into an asynchronous transition system such that the result is history-preserving bisimilar; this construction can help to find a history-preserving bisimilar net (with internal transitions).

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. BBD95.
    E. Badouel, L. Bernardinello, and P. Darondeau. Polynomial algorithms for the synthesis of bounded nets. In P. Mosses et al., editors, TAPSOFT 95, Lect. Notes Comp. Sci. 915, 364–378. Springer, 1995.Google Scholar
  2. BDKP91.
    E. Best, R. Devillers, A. Kiehn, and L. Pomello. Concurrent bisimulations in Petri nets. Acta Informatica, 28:231–264, 1991.zbMATHCrossRefMathSciNetGoogle Scholar
  3. CKLY98.
    J. Cortadella, M. Kishinevsky, L. Lavagno, and A. Yakovlev. Deriving Petri nets from finite transition systems. IEEE Transactions on Computers, 47:859–882, 1998.CrossRefMathSciNetGoogle Scholar
  4. Dar98.
    P. Darondeau. Deriving unbounded Petri nets from formal languages. In D. Sangiorgi and R. de Simone, editors, CONCUR 98, Lect. Notes Comp. Sci. 1466, 533–548. Springer, 1998.Google Scholar
  5. DS93.
    M. Droste and R.M. Shortt. Petri nets and automata with concurrency relations — an adjunction. In M. Droste et al., editors, Semantics of Programming Languages and Model Theory. Gordon and Breach, 69–87. 1993.Google Scholar
  6. GV87.
    R.J. v. Glabbeek and F. Vaandrager. Petri net models for algebraic theories of concurrency. In J.W. de Bakker et al., editors, PARLE Vol. II, Lect. Notes Comp. Sci. 259, 224–242. Springer, 1987.Google Scholar
  7. HKT92.
    P. Hoogers, H. Kleijn, and P.S. Thiagarajan. A trace semantics for Petri nets. In W. Kuich, editor, Automata, Languages and Programming, ICALP 1992, Lect. Notes Comp. Sci. 623, 595–604. Springer, 1992.Google Scholar
  8. NRT92.
    M. Nielsen, G. Rozenberg, and P.S. Thiagarajan. Elementary transition systems. Theor. Comput. Sci., 96:3–33, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  9. NW95.
    M. Nielsen and G. Winskel. Models for concurrency. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science Vol. 4, pages 1–148. Oxford Univ. Press, 1995.Google Scholar
  10. PKY95.
    M. Pietkiewicz-Koutny and A. Yakovlev. Non-pure nets and their transition systems. Technical Report TR 528, Dept. Comp. Sci., Univ. of Newcastle upon Tyne, 1995.Google Scholar
  11. Sun98.
    K. Sunesen. Reasoning about Reactive Systems. PhD thesis, Univ. Aarhus, 1998.Google Scholar
  12. Vog92.
    W. Vogler. Modular Construction and Partial Order Semantics of Petri Nets. Lect. Notes Comp. Sci. 625. Springer, 1992.Google Scholar
  13. Vog95.
    W. Vogler. Timed testing of concurrent systems. Information and Computation, 121:149–171, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  14. Yak98.
    A. Yakovlev. Designing control logic for counterflow pipeline processor using Petri nets. Formal Methods in System Design, 12:39–71, 1998.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Walter Vogler
    • 1
  1. 1.Institut für InformatikUniversität AugsburgGermany

Personalised recommendations