Local model checking for infinite state spaces

Julian Bradfield; Colin Stirling

doi:10.1016/0304-3975(92)90183-G

Local model checking for infinite state spaces

Research output: Contribution to journal › Article › peer-review

Abstract

We present a sound and complete tableau proof system for establishing whether a set of elements of an arbitrary transition system model has a property expressed in (a slight extension of) the modal mu-calculus. The proof system, we believe, offers a very general verification method applicable to a wide range of computational systems.

Original language	English
Pages (from-to)	157 - 174
Journal	Theoretical Computer Science
Volume	96
Issue number	1
DOIs	https://doi.org/10.1016/0304-3975(92)90183-G
Publication status	Published - 1992

Access to Document

10.1016/0304-3975(92)90183-G

Local model checking for infinite state spaces
Open archive
Final published version, 971 KB

http://www.sciencedirect.com/science/article/pii/030439759290183G

Cite this

@article{0c9943590976486ab898af9b70bbff9f,

title = "Local model checking for infinite state spaces",

abstract = "We present a sound and complete tableau proof system for establishing whether a set of elements of an arbitrary transition system model has a property expressed in (a slight extension of) the modal mu-calculus. The proof system, we believe, offers a very general verification method applicable to a wide range of computational systems.",

author = "Julian Bradfield and Colin Stirling",

note = "Selected Papers of the 2nd Workshop on Concurrency and Compositionality",

year = "1992",

doi = "10.1016/0304-3975(92)90183-G",

language = "English",

volume = "96",

pages = "157 -- 174",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier",

number = "1",

}

TY - JOUR

T1 - Local model checking for infinite state spaces

AU - Bradfield, Julian

AU - Stirling, Colin

N1 - Selected Papers of the 2nd Workshop on Concurrency and Compositionality

PY - 1992

Y1 - 1992

N2 - We present a sound and complete tableau proof system for establishing whether a set of elements of an arbitrary transition system model has a property expressed in (a slight extension of) the modal mu-calculus. The proof system, we believe, offers a very general verification method applicable to a wide range of computational systems.

AB - We present a sound and complete tableau proof system for establishing whether a set of elements of an arbitrary transition system model has a property expressed in (a slight extension of) the modal mu-calculus. The proof system, we believe, offers a very general verification method applicable to a wide range of computational systems.

U2 - 10.1016/0304-3975(92)90183-G

DO - 10.1016/0304-3975(92)90183-G

M3 - Article

SN - 0304-3975

VL - 96

SP - 157

EP - 174

JO - Theoretical Computer Science

JF - Theoretical Computer Science

IS - 1

ER -

Local model checking for infinite state spaces

Abstract

Access to Document

Fingerprint

Cite this