sitemap

contact

legal notice

University of Stuttgart

	Institute of Formal Methods in Computer Science
	Software Reliability and Security Group

Partial-order verification techniques (Bibliography)

AIN00

P. A. Abdulla, S. P. Iyer, and A. Nylén.
Unfoldings of Unbounded Petri Nets.
In Proc. of CAV '00, volume 1855 of Lecture Notes in Computer Science, pages 495-507. Springer-Verlag, 2000.

BCM99

P. Baldan, A. Corradini, and U. Montanari.
Unfolding and Event Structure Semantics for Graph Grammars.
In Proc. of FOSSACS '99, volume 1578 of Lecture Notes in Computer Science, pages 367-386. Springer-Verlag, 1999.

Bes97

E. Best.
Partial order verification with PEP.
In DIMACS Series in Discrete Mathematics and Theoretical Computer Science, volume 29, pages 305-328, 1997.

BD87

E. Best and R. Devillers.
Sequential and concurrent behavior in Petri net theory.
Theoretical Computer Science, 55:87-136, 1987.

BG95

E. Best and B. Grahlmann.
Pep: Documentation and user guide.
Universität Hildesheim.
Available together with the tool via: http://theoretica.informatik.uni-oldenburg.de/ $∼$ pep.

BJ97

R. Boubour and C. Jard.
Fault detection in telecommunication networks based on Petri net representation of alarm propagation.
In G. Balbo and P. Azéma, editors, Application and Theory of Petri Nets 1997, volume 1248 of Lecture Notes in Computer Science, pages 367-386. Springer-Verlag, 1997.

CGP00

J.M. Couvreur, S. Grivet, and D. Poitrenaud.
Designing an LTL model checker based on unfolding graphs.
In M. Nielsen and D. Simpson, editors, Application and Theory of Petri Nets 2000, volume 1825 of Lecture Notes in Computer Sciences, pages 123-145. Springer-Verlag, 2000.

CP96

J.M. Couvreur and D. Poitrenaud.
Model checking based on occurrence net graph.
In R. Gotzhein and J. Bredereke, editors, Proc. Formal Description Techniques IX, Theory, Application and Tools, FORTE/PSTV'96, pages 380-395, Kaiserslautern, Germany, October 1996. Chapman and Hall.

Eng91

J. Engelfriet.
Branching processes of Petri nets.
Acta Informatica, 28:575-591, 1991.

Esp94

J. Esparza.
Model checking using net unfoldings.
Science of Computer Programming, 23(2):151-195, 1994.
Also appeared in Proc. TAPSOFT '93, volume 668 of Lecture Notes in Computer Science, pages 613-628. Springer-Verlag, 1993.

EK00

J. Esparza and K. Heljanko.
A New Unfolding Approach to LTL Model Checking.
In Proc. ICALP 2000, volume 1853 of Lecture Notes in Computer Science, pages 475-486. Springer-Verlag, 2000.
Available at http://wwwbrauer.informatik.tu-muenchen.de/gruppen/theorie/publications/.

ERV97

J. Esparza, S. Römer, and W. Vogler.
An improvement of mcmillan's unfolding algorithm.
In Proc. TACAS '96, volume 1055 of Lecture Notes in Computer Science, pages 87-106. Springer-Verlag, 1997.

Gog74

J. Goguen.
On homomorphisms, correctness, termination, unfoldments and equivalence of flow diagram programs.
Jounal of Computer and System Sciences, 8(3):333-365, 1974.

Gra95

B. Grahlmann.
Verifying Telecommunication Protocols with PEP.
In Proceedings of RELECTRONIC'95 (Ninth Symposium on Quality and Reliability in Electronics), pages 251-256, Budapest Hungary, October 1995. Scientific Society for Telecommunications.

Gra97

B. Grahlmann.
The pep tool.
In O. Grumberg, editor, Proceedings of CAV'97 (Computer Aided Verification), volume 1254 of Lecture Notes in Computer Science, pages 440-443. Springer-Verlag, June 1997.

GP98

B. Grahlmann and C. Pohl.
Profiting from SPIN in PEP.
In Proceedings of the SPIN'98 Workshop, November 1998.

Gra97b

B. Graves.
Computing reachability properties hidden in finite net unfoldings.
In S. Ramesh and G. Sivakumar, editors, Proceedings of FST&TCS'97 (Foundations of Software Technology and Theoretical Computer Science), volume 1346 of Lecture Notes in Computer Science, pages 327-341. Springer-Verlag, December 1997.

Gun1993

J. Gunawardena.
A generalized event structure for the Muller unfolding of a safe net.
In Proc. CONCUR'93, 4th International Conference on Concurrency Theory, volume 715 of Lecture Notes in Computer Science, pages 278-292, Hildesheim, Germany, August 1993. Springer-Verlag.

Haa98a

S. Haar.
Branching Processes of general S/T-Systems.
In P. Jancar and M. Krétinský, editors, Proceedings of the Concurrency Workshop at MFCS '98, Brno, Czech Republic, 1998. Faculty of Informatics, Masaryk University.
Report FIMU-RS-98-06.

Haa98b

S. Haar.
Branching Processes of general S/T-Systems and their properties.
In P. Jancar and M. Krétinský, editors, Proc. of MFCS Workshop on Concurrency, Brno '98, volume 18 of ENTCS, URL: http://www.elsevier.nl/locate/entcs/volume18.html, 1998. Elsevier.

HD96

M. Heiner and P. Deussen.
Petri Net Based Design and Analysis of Reactive Systems.
In Proceedings of WODES'96 (Workshop on Discrete Event Systems, Edinburgh), pages 308-313. The Institution of Electrical Engineers, London, 1996.

Hel98

K. Heljanko.
Deadlock checking for complete finite prefixes using logic programs with stable model semantics (extended abstract).
In Proceedings of the Workshop Concurrency, Specification & Programming 1998, Informatik-Bericht Nr. 110, pages 106-115. Humboldt-University, Berlin, September 1998.
Available at http://www.tcs.hut.fi/ kepa/publications/KH_csp98.ps.gz.

Hel99

K. Heljanko.
Using logic programs with stable model semantics to solve deadlock and reachability problems for 1-safe petri nets.
In Proceedings of Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99), volume 1579 of Lecture Notes in Computer Science, pages 240-254. Springer-Verlag, 1999.

Hel00

K. Heljanko.
Model checking with finite complete prefixes is PSPACE-complete.
In Catuscia Palamidessi, editor, Proceedings of the 11th International Conference on Concurrency Theory (Concur'2000), volume 1877 of Lecture Notes in Computer Science, pages 108-122, State College, Pennsylvania, USA, August 2000. Springer, Berlin.

Hen97

O. Henniger.
On test case generation from asynchronously communicating state machines.
In M. Kim, S. Kang, and K. Hong, editors, Testing of Communicating Systems, X, Cheju Island, South Korea, 1997. Chapman & Hall.
Available at http://www.darmstadt.gmd.de/ henniger/publications/hen97.ps.

Hoo94

P. Hoogers.
Behavioural Aspects of Petri Nets.
Ph. d. thesis, University of Leiden, Leiden, Netherlands, 1994.
Available under ftp://ftp.wi.leidenuniv.nl/pub/CS/PhDTheses/ hoogers-94.ps.gz.

HKT93

P. W. Hoogers, H. C. M. Kleijn, and P. S. Thiagarajan.
Local event structures and Petri nets.
In Proc. CONCUR'93, 4th International Conference on Concurrency Theory, volume 715 of Lecture Notes in Computer Science, pages 462-476, Hildesheim, Germany, August 1993. Springer-Verlag.

HKT95

P. W. Hoogers, H. C. M. Kleijn, and P. S. Thiagarajan.
A Trace Semantics for Petri Nets.
Information and Computation, 117:98-114, 1995.

HKT96

P.W. Hoogers, H.C.M. Kleijn, and P.S. Thiagarajan.
An Event Structure Semantics for General Petri Nets.
Theoretical Computer Science, 153:129-170, 1996.

HNW98

M. Huhn, P. Niebert, and F. Wallner.
Verification based on local states.
In Proceedings of TACAS '98, volume 1384 of Lecture Notes in Computer Science, pages 36-51. Springer-Verlag, 1998.

HNW99

Michaela Huhn, Peter Niebert, and Frank Wallner.
Model checking logics for communicating agents.
volume 1578 of Lecture Notes in Computer Science, pages 227-242. Springer-Verlag, 99.

KKTV94

M. Kishinevsky, A. Kondratyev, A. Taubin, and V. Varshavsky.
Concurrent Hardware: The Theory and Practice of Self-Timed Design.
Series in Parallel Computing. John Wiley & Sons, 1994.
Book can be ordered: http://www.amazon.com/exec/obidos/ts/book-contents/0471935360/distributednet/002-4460350-6555426.

KMR98

H.C.M. Kleijn, R. Morin, and B. Rozoy.
Event Structures for Local Traces.
Electronic Notes in Theoretical Computer Science, 16(2), 1998.
Available at http://www.elsevier.nl/locate/entcs/volume16.html and as Leiden University Technical Report 98-10.

KCKLTY98

A. Kondratyev, J. Cortadella, M. Kishinevsky, L. Lavagno, A. Taubin, and A. Yakovlev.
Identifying state coding conflicts in asynchronous system specifications using Petri net unfoldings.
In International Conference on Application of Concurrency to System Design, pages 152-163, Japan, March 1998.

KKTCL98

A. Kondratyev, M. Kishinevsky, A. Taubin, J. Cortadella, and L. Lavagno.
The use of Petri nets for the design and verification of asynchronous circuits and systems.
Journal of Circuits, Systems, and Computers, 8(1):67-118, 1998.

KKTT96

A. Kondratyev, M. Kishinevsky, A. Taubin, and S. Ten.
A Structural Approach for the Analysis of Petri Nets byReduced Unfoldings.
In 17th International Conference on Application and Theory of Petri Nets, pages 346-365, Osaka, Japan, June 1996.

KKTT98

A. Kondratyev, M. Kishinevsky, A. Taubin, and S. Ten.
Analysis of Petri nets by ordering relations in reduced unfoldings.
Formal Methods in System Design, 12(1):5-38, 1998.

KT94

A. Kondratyev and A. Taubin.
On verification of the speed-independent circuits by STG unfoldings.
In International Symposium on Advanced Research in Asynchronous Circuits and Systems, Salt Lake City, Utah, USA, November 1994.

KTT94

Alex Kondratyev, Alexander Taubin, and Sergey Ten.
Verification of Asynchronous Circuits by Petri Net Unfoldings.
In 1994 IEEE Symposium on Emerging Technologies and Factory Automation, ETFA'94, pages 404-413, November 1994.

McM92

K.L. McMillan.
Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits.
In Proc. CAV '92, Fourth Workshop on Computer-Aided Verification, volume 663 of Lecture Notes in Computer Science, pages 164-174, 1992.
no abstract.

McM93

K.L. McMillan.
Symbolic Model Checking.
Kluwer, 1993.

McM95b

K.L. McMillan.
A technique of state space search based on unfolding.
Formal Methods in System Design, 6(1):45-65, 1995.

McM95a

K.L. McMillan.
Trace theoretic verification of asynchronous circuits using unfoldings.
In Proc. CAV '95, 7th International Conference on Computer-Aided Verification, volume 939 of Lecture Notes in Computer Science, pages 180-195. Springer-Verlag, 1995.

MR97

S. Melzer and S. Römer.
Deadlock checking using net unfoldings.
In Proc. CAV'97, International Conference on Computer-Aided Verification, volume 1254 of Lecture Notes in Computer Science, pages 352-363, Haifa, Israel, 1997. Springer-Verlag.

MRE96

S. Melzer, S. Römer, and J. Esparza.
Verification using PEP.
In Proc. AMAST '96, volume 1101 of Lecture Notes in Computer Science, pages 591-594. Springer-Verlag, 1996.

MMS92

J. Meseguer, U. Montanari, and V. Sassone.
On the semantics of petri nets.
In Proceedings of the 3rd International Conference on Concurrency Theory, CONCUR `92, volume 630 of Lecture Notes in Computer Science, pages 286-301. Springer-Verlag, 1992.

MMS94

J. Meseguer, U. Montanari, and V. Sassone.
On the model of computation of place/transition petri nets.
In Proceedings of the 15th International Conference on Application and Theory of Petri Nets, volume 815 of Lecture Notes in Computer Science, pages 16-38. Springer-Verlag, 1994.

MMS96

J. Meseguer, U. Montanari, and V. Sassone.
Process versus unfolding semantics for place/transition petri nets.
Theoretical Computer Science, 153(1-2):171-210, 1996.

MMS97

J. Meseguer, U. Montanari, and V. Sassone.
On the semantics of place/transition petri nets.
Mathematical Structures in Computer Science, 7:359-397, 1997.

NPW80

M. Nielsen, G. Plotkin, and G. Winskel.
Petri Nets, Event Structures and Domains.
Theoretical Computer Science, 13(1):85-108, 1980.

Poi96

D. Poitrenaud.
Graphes de Processus Arborescents pour la Vérification de Propriétés de Systèmes Concurrents.
Thèse de doctorat, Université P. et M. Curie, Paris, France, December 1996.

Roe96

S. Römer.
An efficient algorithm for the computation of unfoldings of finite and safe Petri nets (on efficiently implementing McMillan's unfolding algorithm).
Technical report, Technishe Universität München, Institut für Informatik, 1996.

Sem97

A. Semenov.
Verification and Synthesis of Asynchronous Control Circuits using Petri Net Unfoldings.
PhD thesis, University of Newcastle upon Tyne, 1997.

SY95

A. Semenov and A. Yakovlev.
Combining partial orders and symbolic traversal for efficient verification of asynchronous circuits.
In Proc. IFIP Int. Conference on Computer Hardware Description Languages, (CHDL'95),Chiba, Japan, pages 567-573, August-September 1995.

SY96

A. Semenov and A. Yakovlev.
Verification of asynchronous circuits based on timed petri net unfolding.
In Proc. DAC'96, Las Vegas, pages 59-63, June 1996.

SYPPCL97

A. Semenov, A. Yakovlev, E. Pastor, M. Pena, J. Cortadella, and L. Lavagno.
Partial order approach to synthesis of speed-independent circuits.
In Proc. 3rd Int. Symp. on Advanced Research in Asynchronous Circuits and Systems, pages 254-265, Eindhoven, Holland, April 1997. IEEE Comp. Soc. Press.

TKK98

A. Taubin, M. Kishinevsky, and A. Kondratyev.
Deadlock prevention using petri nets and their unfoldings.
International Journal of Advanced Manufacturing Technology, 14(10):750-759, 1998.

TKK96

A. Taubin, A. Kondratyev, and M. Kishinevsky.
Deadlock prevention using Petri net unfoldings.
In Proc. CESA' 96 IMACS Multiconference. Symposium on Discrete Events and Manufacturing Systems, pages 426-431, Lille, France, July 1996.

TKK97

A. Taubin, A. Kondratyev, and M. Kishinevsky.
Applications of petri nets unfoldings to asynchronous design.
In 1997 IEEE International Conference on Systems, Man, and Cybernetics, volume 5, pages 4279-4284, Orlando, Florida, October 1997.

Ulr97

A. Ulrich.
A description model to support test suite derivation for concurrent systems.
In M. Zitterbart, editor, 10. GI/ITG-Fachtagung Kommunikation in Verteilten Systemen, Braunschweig, Germany, 1997.

VSY98

W. Vogler, A. Semenov, and A. Yakovlev.
Unfolding and finite prefix for nets with read arcs.
In D. Sangiorgi and R. de Simone, editors, CONCUR 98, LNCS 1466, 501-516. Springer, 1998.
Full version as Technical Report Series No. 634, Computing Science, University of Newcastle upon Tyne, February 1998; can be obtained from: ftp://sadko.ncl.ac.uk/pub/incoming/TRs/.

Wal98

F. Wallner.
Model-checking LTL using net unfoldings.
In Proc. CAV '95, 10th International Conference on Computer-Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 207-218, Vancouver, Canada, 1998.

Software Reliability and Security Group

Partial-order verification techniques (Bibliography)