Generating and Exploiting State Spaces of Object-Oriented Petri Nets

Type

conference paper

Language

English

Authors

Češka Milan, prof. RNDr., CSc.
Janoušek Vladimír, doc. Ing., Ph.D.
Vojnar Tomáš, prof. Ing., Ph.D., FEEC (FEEC)

Abstract

The article describes two of the problems arising in the area of generating and exploiting state spaces of the object-oriented Petri nets (OOPNs) associated to the tool called PNtalk. Firstly, the influence of identifiers of dynamically appearing and disappearing instances upon the state space explosion problem is explained. Methods of working with identifiers based on sophisticated naming rules and mechanisms for abstracting names are described and compared. Subsequently, there are discussed several attitudes to specifying properties of systems to be validated by means of state spaces of their OOPN-based models.

Keywords

Petri nets, object-orientation, formal analysis and verification

Annotation

The article describes two of the problems arising in the area of generating and exploiting state spaces of the object-oriented Petri nets (OOPNs) associated to the tool called PNtalk. Firstly, the influence of identifiers of dynamically appearing and disappearing instances upon the state space explosion problem is explained. Methods of working with identifiers based on sophisticated naming rules and mechanisms for abstracting names are described and compared. Subsequently, there are discussed several attitudes to specifying properties of systems to be validated by means of state spaces of their OOPN-based models.

Published

2000

Pages

35–54

Journal

DAIMI PB, no. DAIMI PB, ISSN 0105-8517

Proceedings

Proceedings of Workshop on Software Engineering and Petri Nets, 21st International Conference on Application and Theory of Petri Nets 2000

Publisher

unknown

Place

Aarhus

BibTeX

@inproceedings{BUT191471,
  author="Milan {Češka} and Vladimír {Janoušek} and Tomáš {Vojnar}",
  title="Generating and Exploiting State Spaces of Object-Oriented Petri Nets",
  booktitle="Proceedings of Workshop on Software Engineering and Petri Nets, 21st International Conference on Application and Theory of Petri Nets 2000",
  year="2000",
  journal="DAIMI PB",
  number="DAIMI PB",
  pages="35--54",
  publisher="unknown",
  address="Aarhus",
  issn="0105-8517"
}

Projects

Modelling, Verifying, and Prototyping Distributed Applications Using Petri Nets, GACR, Standardní projekty, GA102/00/1017, start: 2000-01-01, end: 2002-12-31, completed
PNtalk - tools based on object-oriented Petri nets, BUT, Institucionální podpora na rozvoj výzkumné organizace, UIVT-PNtalk, start: 1994-01-01, end: 2010-12-31, completed

Research groups

Petri Nets Research Group (RG PETRINET)
System Modelling and Optimization Research Group (RG MODSIM)

Departments

Faculty of Information Technology (FIT)