Publication detail

Partial Order Reduction in Model Checking of Object-Oriented Petri Nets

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

Original Title

Partial Order Reduction in Model Checking of Object-Oriented Petri Nets

English Title

Partial Order Reduction in Model Checking of Object-Oriented Petri Nets

Type

conference paper

Language

en

Original Abstract

In this paper, we discuss some on-the-fly methods for model checking over OOPNs, i.e. methods in which generation of state spaces is done simultaneously with (and is guided by) checking the appropriate property. A big challenge in finite-state model checking is the state space explosion problem, i.e. the exponential growth of state spaces. Fortunately, there have been proposed many advanced methods for reducing state spaces. One of the most successful methods (especially when dealing with software systems) is the so-called partial-order reduction. We examine how this method can be used in the context of OOPNs, which bring in features like dynamic instantiation, late binding, garbage collection, etc.

English abstract

In this paper, we discuss some on-the-fly methods for model checking over OOPNs, i.e. methods in which generation of state spaces is done simultaneously with (and is guided by) checking the appropriate property. A big challenge in finite-state model checking is the state space explosion problem, i.e. the exponential growth of state spaces. Fortunately, there have been proposed many advanced methods for reducing state spaces. One of the most successful methods (especially when dealing with software systems) is the so-called partial-order reduction. We examine how this method can be used in the context of OOPNs, which bring in features like dynamic instantiation, late binding, garbage collection, etc.

Keywords

object-oriented Petri nets, formal analysis and verification, state space, model checking, partial order reduction

RIV year

2003

Released

24.02.2003

Publisher

University of Las Palmas

Location

Las Palmas de Gran Canaria, Canary Islands

ISBN

84-688-0820-2

Book

Cast and Complexity in Biological, Physical and Engineering Systems, Extended Abstracts, Eurocast 2003

Pages from

254

Pages to

256

Pages count

3

Documents

BibTex


@inproceedings{BUT13953,
  author="Milan {Češka} and Luděk {Haša} and Tomáš {Vojnar}",
  title="Partial Order Reduction in Model Checking of Object-Oriented Petri Nets",
  annote="In this paper, we discuss some on-the-fly methods for model checking
over OOPNs, i.e. methods in which generation of state spaces is done
simultaneously with (and is guided by) checking the appropriate
property. A big challenge in finite-state model checking is the state
space explosion problem, i.e. the exponential growth of state spaces.
Fortunately, there have been proposed many advanced methods for
reducing state spaces. One of the most successful methods (especially
when dealing with software systems) is the so-called partial-order
reduction. We examine how this method can be used in the context of
OOPNs, which bring in features like dynamic instantiation, late
binding, garbage collection, etc.",
  address="University of Las Palmas",
  booktitle="Cast and Complexity in Biological, Physical and Engineering Systems, Extended Abstracts, Eurocast 2003",
  chapter="13953",
  institution="University of Las Palmas",
  year="2003",
  month="february",
  pages="254--256",
  publisher="University of Las Palmas",
  type="conference paper"
}