Faster SPDL Model Checking Through Property-Driven State Space Generation

Matthias Kuntz; Boudewijn R. Haverkort

doi:10.1007/978-3-540-75211-0_7

Faster SPDL Model Checking Through Property-Driven State Space Generation

Matthias Kuntz, Boudewijn R. Haverkort

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

66 Downloads (Pure)

Abstract

In this paper we describe how both, memory and time requirements for stochastic model checking of SPDL (stochastic propositional dynamic logic) formulae can significantly be reduced. SPDL is the stochastic extension of the multi-modal program logic PDL. SPDL provides means to specify path-based properties with or without timing restrictions. Paths can be characterised by so-called programs, essentially regular expressions, where the executability can be made dependent on the validity of test formulae. For model-checking SPDL path formulae it is necessary to build a product transition system (PTS) between the system model and the program automaton belonging to the path formula that is to be verified. In many cases, this PTS can be drastically reduced during the model checking procedure, as the program restricts the number of potentially satisfying paths. Therefore, we propose an approach that directly generates the reduced PTS from a given SPA specification and an SPDL path formula. The feasibility of this approach is shown through a selection of case studies, which show enormous state space reductions, at no increase in generation time.

Original language	English
Title of host publication	Formal Methods and Stochastic Models for Performance Evaluation
Subtitle of host publication	Fourth European Performance Engineering Workshop, EPEW 2007, Berlin, Germany, September 27-28, 2007. Proceedings
Editors	Katinka Wolter
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	80-96
Number of pages	17
ISBN (Print)	978-3-540-75210-3
DOIs	https://doi.org/10.1007/978-3-540-75211-0_7
Publication status	Published - 14 Sept 2007
Event	4th European Performance Engineering Workshop, EPEW 2007 - Berlin, Germany Duration: 27 Sept 2007 → 28 Sept 2007 Conference number: 4

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	4748
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Workshop

Workshop	4th European Performance Engineering Workshop, EPEW 2007
Abbreviated title	EPEW
Country/Territory	Germany
City	Berlin
Period	27/09/07 → 28/09/07

Keywords

Model check
Parse tree
Kanban system
State space generation
Propositional dynamic logic

Access to Document

10.1007/978-3-540-75211-0_7

Kuntz2007fasterAccepted author version, 216 KB

Cite this

Kuntz, M., & Haverkort, B. R. (2007). Faster SPDL Model Checking Through Property-Driven State Space Generation. In K. Wolter (Ed.), Formal Methods and Stochastic Models for Performance Evaluation: Fourth European Performance Engineering Workshop, EPEW 2007, Berlin, Germany, September 27-28, 2007. Proceedings (pp. 80-96). (Lecture Notes in Computer Science; Vol. 4748). Springer. https://doi.org/10.1007/978-3-540-75211-0_7

Kuntz, Matthias ; Haverkort, Boudewijn R. / Faster SPDL Model Checking Through Property-Driven State Space Generation. Formal Methods and Stochastic Models for Performance Evaluation: Fourth European Performance Engineering Workshop, EPEW 2007, Berlin, Germany, September 27-28, 2007. Proceedings. editor / Katinka Wolter. Berlin, Heidelberg : Springer, 2007. pp. 80-96 (Lecture Notes in Computer Science).

@inproceedings{2aa8f6c5e4dd4ef8a1fc9c7d5740cebb,

title = "Faster SPDL Model Checking Through Property-Driven State Space Generation",

abstract = "In this paper we describe how both, memory and time requirements for stochastic model checking of SPDL (stochastic propositional dynamic logic) formulae can significantly be reduced. SPDL is the stochastic extension of the multi-modal program logic PDL. SPDL provides means to specify path-based properties with or without timing restrictions. Paths can be characterised by so-called programs, essentially regular expressions, where the executability can be made dependent on the validity of test formulae. For model-checking SPDL path formulae it is necessary to build a product transition system (PTS) between the system model and the program automaton belonging to the path formula that is to be verified. In many cases, this PTS can be drastically reduced during the model checking procedure, as the program restricts the number of potentially satisfying paths. Therefore, we propose an approach that directly generates the reduced PTS from a given SPA specification and an SPDL path formula. The feasibility of this approach is shown through a selection of case studies, which show enormous state space reductions, at no increase in generation time.",

keywords = "Model check, Parse tree, Kanban system, State space generation, Propositional dynamic logic",

author = "Matthias Kuntz and Haverkort, {Boudewijn R.}",

year = "2007",

month = sep,

day = "14",

doi = "10.1007/978-3-540-75211-0_7",

language = "English",

isbn = "978-3-540-75210-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "80--96",

editor = "Katinka Wolter",

booktitle = "Formal Methods and Stochastic Models for Performance Evaluation",

address = "Germany",

note = "4th European Performance Engineering Workshop, EPEW 2007, EPEW ; Conference date: 27-09-2007 Through 28-09-2007",

}

Kuntz, M & Haverkort, BR 2007, Faster SPDL Model Checking Through Property-Driven State Space Generation. in K Wolter (ed.), Formal Methods and Stochastic Models for Performance Evaluation: Fourth European Performance Engineering Workshop, EPEW 2007, Berlin, Germany, September 27-28, 2007. Proceedings. Lecture Notes in Computer Science, vol. 4748, Springer, Berlin, Heidelberg, pp. 80-96, 4th European Performance Engineering Workshop, EPEW 2007, Berlin, Berlin, Germany, 27/09/07. https://doi.org/10.1007/978-3-540-75211-0_7

Faster SPDL Model Checking Through Property-Driven State Space Generation. / Kuntz, Matthias; Haverkort, Boudewijn R.
Formal Methods and Stochastic Models for Performance Evaluation: Fourth European Performance Engineering Workshop, EPEW 2007, Berlin, Germany, September 27-28, 2007. Proceedings. ed. / Katinka Wolter. Berlin, Heidelberg: Springer, 2007. p. 80-96 (Lecture Notes in Computer Science; Vol. 4748).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Faster SPDL Model Checking Through Property-Driven State Space Generation

AU - Kuntz, Matthias

AU - Haverkort, Boudewijn R.

N1 - Conference code: 4

PY - 2007/9/14

Y1 - 2007/9/14

N2 - In this paper we describe how both, memory and time requirements for stochastic model checking of SPDL (stochastic propositional dynamic logic) formulae can significantly be reduced. SPDL is the stochastic extension of the multi-modal program logic PDL. SPDL provides means to specify path-based properties with or without timing restrictions. Paths can be characterised by so-called programs, essentially regular expressions, where the executability can be made dependent on the validity of test formulae. For model-checking SPDL path formulae it is necessary to build a product transition system (PTS) between the system model and the program automaton belonging to the path formula that is to be verified. In many cases, this PTS can be drastically reduced during the model checking procedure, as the program restricts the number of potentially satisfying paths. Therefore, we propose an approach that directly generates the reduced PTS from a given SPA specification and an SPDL path formula. The feasibility of this approach is shown through a selection of case studies, which show enormous state space reductions, at no increase in generation time.

AB - In this paper we describe how both, memory and time requirements for stochastic model checking of SPDL (stochastic propositional dynamic logic) formulae can significantly be reduced. SPDL is the stochastic extension of the multi-modal program logic PDL. SPDL provides means to specify path-based properties with or without timing restrictions. Paths can be characterised by so-called programs, essentially regular expressions, where the executability can be made dependent on the validity of test formulae. For model-checking SPDL path formulae it is necessary to build a product transition system (PTS) between the system model and the program automaton belonging to the path formula that is to be verified. In many cases, this PTS can be drastically reduced during the model checking procedure, as the program restricts the number of potentially satisfying paths. Therefore, we propose an approach that directly generates the reduced PTS from a given SPA specification and an SPDL path formula. The feasibility of this approach is shown through a selection of case studies, which show enormous state space reductions, at no increase in generation time.

KW - Model check

KW - Parse tree

KW - Kanban system

KW - State space generation

KW - Propositional dynamic logic

U2 - 10.1007/978-3-540-75211-0_7

DO - 10.1007/978-3-540-75211-0_7

M3 - Conference contribution

SN - 978-3-540-75210-3

T3 - Lecture Notes in Computer Science

SP - 80

EP - 96

BT - Formal Methods and Stochastic Models for Performance Evaluation

A2 - Wolter, Katinka

PB - Springer

CY - Berlin, Heidelberg

T2 - 4th European Performance Engineering Workshop, EPEW 2007

Y2 - 27 September 2007 through 28 September 2007

ER -

Kuntz M, Haverkort BR. Faster SPDL Model Checking Through Property-Driven State Space Generation. In Wolter K, editor, Formal Methods and Stochastic Models for Performance Evaluation: Fourth European Performance Engineering Workshop, EPEW 2007, Berlin, Germany, September 27-28, 2007. Proceedings. Berlin, Heidelberg: Springer. 2007. p. 80-96. (Lecture Notes in Computer Science). doi: 10.1007/978-3-540-75211-0_7

Faster SPDL Model Checking Through Property-Driven State Space Generation

Abstract

Publication series

Workshop

Keywords

Access to Document

Fingerprint

Cite this