Sciweavers

Share
IJCAI
2003
8 years 4 months ago
Formal Verification of Diagnosability via Symbolic Model Checking
This paper addresses the formal verification of diagnosis systems. We tackle the problem of diagnosability: given a partially observable dynamic system, and a diagnosis system obs...
Alessandro Cimatti, Charles Pecheur, Roberto Cavad...
BCS
2008
8 years 4 months ago
On the Complexity of Parity Games
Parity games underlie the model checking problem for the modal
Arnold Beckmann, Faron Moller
ERSHOV
2006
Springer
8 years 5 months ago
Well-Structured Model Checking of Multiagent Systems
Abstract. We address model checking problem for combination of Computation Tree Logic (CTL) and Propositional Logic of Knowledge (PLK) in finite systems with the perfect recall syn...
Nikolay V. Shilov, Natalya Olegovna Garanina
ICALP
2000
Springer
8 years 6 months ago
A New Unfolding Approach to LTL Model Checking
Abstract A new unfolding approach to LTL model checking is presented, in which the model checking problem can be solved by direct inspection of a certain finite prefix. The techniq...
Javier Esparza, Keijo Heljanko
FSTTCS
2006
Springer
8 years 7 months ago
On Decidability of LTL Model Checking for Process Rewrite Systems
We establish a decidability boundary of the model checking problem for infinite-state systems defined by Process Rewrite Systems (PRS) or weakly extended Process Rewrite Systems (w...
Laura Bozzelli, Mojmír Kretínsk&yacu...
CONCUR
2004
Springer
8 years 7 months ago
A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications
We introduce a generic family of behavioral relations for which the problem of comparing an arbitrary transition system to some finite-state specification can be reduced to a model...
Antonín Kucera, Ph. Schnoebelen
ICALP
2003
Springer
8 years 8 months ago
Quantitative Analysis of Probabilistic Lossy Channel Systems
Many protocols are designed to operate correctly even in the case where the underlying communication medium is faulty. To capture the behaviour of such protocols, lossy channel sy...
Alexander Moshe Rabinovich
CAV
2003
Springer
160views Hardware» more  CAV 2003»
8 years 8 months ago
Fast Mu-Calculus Model Checking when Tree-Width Is Bounded
We show that the model checking problem for µ-calculus on graphs of bounded tree-width can be solved in time linear in the size of the system. The result is presented by first sh...
Jan Obdrzálek
IFIP
2004
Springer
8 years 8 months ago
Static program transformations for efficient software model checking
Ensuring correctness of software by formal methods is a very relevant and widely studied problem. Automatic verification of software using model checkers from the state space exp...
Shobha Vasudevan, Jacob A. Abraham
FMCAD
2004
Springer
8 years 8 months ago
Simple Bounded LTL Model Checking
We present a new and very simple translation of the bounded model checking problem which is linear both in the size of the formula and the length of the bound. The resulting CNF-fo...
Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A...
books