Publication detail

Improvements in Model Checking for Object-Oriented Petri Nets

HAŠA, L., ČEŠKA, M.

Original Title

Improvements in Model Checking for Object-Oriented Petri Nets

English Title

Improvements in Model Checking for Object-Oriented Petri Nets

Type

conference paper

Language

en

Original Abstract

Safety and liveness properties can be expressed by LTL\X in model checking of a concurrent system. However, common logics, and LTL\X is ranked among them, do not provide tools for tracing particular instances along state space paths. For this reason, an indexed temporal logic (ICTL) has been introduced into Object-Object Petri Net model checking.
Explicit-state model checking tools often incorporate partial-order reductions to reduce the number of explored states. In this paper, we present a new version of partial order reduction algorithm for LTL\X in the context of Object-Oriented Petri Nets.

English abstract

Safety and liveness properties can be expressed by LTL\X in model checking of a concurrent system. However, common logics, and LTL\X is ranked among them, do not provide tools for tracing particular instances along state space paths. For this reason, an indexed temporal logic (ICTL) has been introduced into Object-Object Petri Net model checking.
Explicit-state model checking tools often incorporate partial-order reductions to reduce the number of explored states. In this paper, we present a new version of partial order reduction algorithm for LTL\X in the context of Object-Oriented Petri Nets.

Keywords

LTL, ICTL, model checking, Object-Oriented Petri Nets, partial-order
reduction, state space

RIV year

2004

Released

30.08.2004

Publisher

The International Institute of Informatics and Systemics

Location

Orlando

ISBN

980-6560-19-1

Book

Proceedings of the ISAS CITSA 2004, Volume III, Communications, Information and Control Systems, Technologies and Applications

Pages from

269

Pages to

274

Pages count

6

Documents

BibTex


@inproceedings{BUT17351,
  author="Luděk {Haša} and Milan {Češka}",
  title="Improvements in Model Checking for Object-Oriented Petri Nets",
  annote="Safety and liveness properties can be expressed by LTL\X in model checking of a concurrent system. However, common logics, and LTL\X is ranked among them, do not provide tools for tracing particular instances along state space paths. For this reason, an indexed temporal logic (ICTL) has been introduced into Object-Object Petri Net model checking.
Explicit-state model checking tools often incorporate partial-order reductions to reduce the number of explored states. In this paper, we present a new version of partial order reduction algorithm for LTL\X in the context of Object-Oriented Petri Nets.", address="The International Institute of Informatics and Systemics", booktitle="Proceedings of the ISAS CITSA 2004, Volume III, Communications, Information and Control Systems, Technologies and Applications", chapter="17351", institution="The International Institute of Informatics and Systemics", year="2004", month="august", pages="269--274", publisher="The International Institute of Informatics and Systemics", type="conference paper" }