Publication Details

Allocational Temporal Logic in Model Checking for Object-Oriented Petri Nets

HAŠA Luděk and ČEŠKA Milan. Allocational Temporal Logic in Model Checking for Object-Oriented Petri Nets. In: Proceedings of 37th International Conference MOSIS´03 Modelling and Simulation of Systems. Ostrava, 2003, pp. 177-182. ISBN 80-85988-86-0.
Czech title
Aplikace alokační temporální logiky při verifikaci OOPN
Type
conference paper
Language
english
Authors
Haša Luděk, Ing. (DITS FIT BUT)
Češka Milan, prof. RNDr., CSc. (DITS FIT BUT)
Keywords

allocational temporal logic, model checking, OOPN, linear temporal logic

Abstract

The basic principles and approaches of model checking for Object-Oriented Petri Nets (OOPNs) are introduced and described in this paper. Specifications of checked properties in model checking are expressed in temporal logics. Allocational temporal logic (ATL) can be used as a formalism to express properties concerning the dynamic allocation and deallocation of entities, such as the objects in an object-based system.

Published
2003
Pages
177-182
Proceedings
Proceedings of 37th International Conference MOSIS´03 Modelling and Simulation of Systems
Conference
MOSIS 2003 - Modelling and Simulation of Systems, Brno, CZ
ISBN
80-85988-86-0
Place
Ostrava, CZ
BibTeX 
@INPROCEEDINGS{FITPUB7188,
   author = "Lud\v{e}k Ha\v{s}a and Milan \v{C}e\v{s}ka",
   title = "Allocational Temporal Logic in Model Checking for Object-Oriented Petri Nets",
   pages = "177--182",
   booktitle = "Proceedings of 37th International Conference MOSIS03 Modelling and Simulation of Systems",
   year = 2003,
   location = "Ostrava, CZ",
   ISBN = "80-85988-86-0",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/7188"
}
Back to top