Decidability of model checking for infinite-state concurrent systems (Q1920224): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
| Property / full work available at URL | |||
| Property / full work available at URL: https://doi.org/10.1007/s002360050074 / rank | |||
Normal rank | |||
| Property / OpenAlex ID | |||
| Property / OpenAlex ID: W1977601940 / rank | |||
Normal rank | |||
Revision as of 21:04, 19 March 2024
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Decidability of model checking for infinite-state concurrent systems |
scientific article |
Statements
Decidability of model checking for infinite-state concurrent systems (English)
0 references
5 June 1997
0 references
We study the model checking problem for linear and branching logics and two models of concurrent computation: Petri nets and basic parallel processes. While Petri nets are a rather powerful model, which can be used to represent and analyse a large variety of systems, basic parallel processes are rather limited. The main results of the paper are that the model checking problem is decidable for an expressive linear time logic (the linear time mu-calculus) and Petri nets, but undecidable for a weak branching time logic (a fragment of UB) and basic parallel processes.
0 references
linear logics
0 references
model checking
0 references
branching logics
0 references
concurrent computation
0 references
Petri nets
0 references
parallel processes
0 references
mu-calculus
0 references
