CAV
2004
Springer
13 years 10 months ago
2004
Springer
—We introduce a new BDD-like data structure called Hybrid-Restriction Diagrams (HRDs) for the representation and manipulation of linear hybrid automata (LHA) state-spaces and pre...
CAV
2004
Springer
13 years 10 months ago
2004
Springer
We show that termination of a class of linear loop programs is decidable. Linear loop programs are discrete-time linear systems with a loop condition governing termination, that is...
CAV
2004
Springer
13 years 10 months ago
2004
Springer
Abstract. Separation Logic consists of a Boolean combination of predicates of the form vi ≥ vj +c where c is a constant and vi, vj are variables of some ordered infinite type li...
CAV
2004
Springer
13 years 10 months ago
2004
Springer
Abstract. We propose a new statistical approach to analyzing stochastic systems against specifications given in a sublogic of continuous stochastic logic (CSL). Unlike past numeri...
CAV
2004
Springer
13 years 10 months ago
2004
Springer
Verifying whether an ω-regular property is satisfied by a finite-state system is a core problem in model checking. Standard techniques build an automaton with the complementary ...
CAV
2004
Springer
13 years 10 months ago
2004
Springer
Abstract. We present an unfolding-based approach to LTL-X modelchecking of high-level Petri nets. It is based on the method proposed by Esparza and Heljanko for low-level nets [4, ...
CAV
2004
Springer
13 years 10 months ago
2004
Springer
This paper reviews the principles behind the paradigm of “abstract interpretation via § -valued logic,” discusses recent work to extend the approach, and summarizes ongoing re...
CAV
2004
Springer
13 years 10 months ago
2004
Springer
CAV
2004
Springer
13 years 10 months ago
2004
Springer
SAL 2 augments the specification language and explicit-state model checker of SAL 1 with high-performance symbolic and bounded model checkers, and with novel infinite bounded and...
CAV
2004
Springer
13 years 10 months ago
2004
Springer
This paper presents a symbolic model checking algorithm for Fixpoint Logic with Chop, an extension of the modal µ-calculus capable of defining non-regular properties. Some empiri...