Sciweavers

CONCUR
2000
Springer
13 years 10 months ago
Model Checking with Finite Complete Prefixes Is PSPACE-Complete
Unfoldings are a technique for verification of concurrent and distributed systems introduced by McMillan. The method constructs a finite complete prefix, which can be seen as a sym...
Keijo Heljanko
FSTTCS
1993
Springer
13 years 11 months ago
Complexity Results for 1-safe Nets
We study the complexity of several standard problems for 1-safe Petri nets and some of its subclasses. We prove that reachability, liveness, and deadlock are all PSPACE-complete f...
Allan Cheng, Javier Esparza, Jens Palsberg
ASP
2001
Springer
13 years 11 months ago
Answer Set Programming and Bounded Model Checking
In this paper bounded model checking of asynchronous concurrent systems is introduced as a promising application area for answer set programming. This is an extension of earlier w...
Keijo Heljanko, Ilkka Niemelä
FSTTCS
2009
Springer
14 years 1 months ago
Modelchecking counting properties of 1-safe nets with buffers in paraPSPACE
ABSTRACT. We consider concurrent systems that can be modelled as 1-safe Petri nets communicating through a fixed set of buffers (modelled as unbounded places). We identify a param...
M. Praveen, Kamal Lodaya