ATVA
2009
Springer
14 years 6 months ago
2009
Springer
Parity games are 2-player games of perfect information and infinite duration that have important applications in automata theory and decision procedures (validity as well as model...
ATVA
2009
Springer
14 years 6 months ago
2009
Springer
In this paper, we describe a decompositional approach to convergence proofs for stochastic hybrid systems given as probabilistic hybrid automata. We focus on a concept called “st...
ATVA
2009
Springer
14 years 6 months ago
2009
Springer
ATVA
2009
Springer
14 years 6 months ago
2009
Springer
: In this paper, we address the problem of synthesizing opaque systems. A secret predicate S over the runs of a system G is opaque to an external user having partial observability ...
ATVA
2009
Springer
14 years 6 months ago
2009
Springer
Weakly relational numeric domains express restricted classes of linear inequalities that strike a balance between what can be described and what can be efficiently computed. Popula...
ATVA
2009
Springer
14 years 6 months ago
2009
Springer
We present a data symmetry reduction approach for model temporal-epistemic logic. The technique abstracts the epistemic indistinguishably relation for the knowledge operators, and ...
ATVA
2009
Springer
14 years 6 months ago
2009
Springer
We present a new approach for automatic verification of data-dependent programs manipulating dynamic heaps. A heap is encoded by a graph where the nodes represent the cells, and t...
ATVA
2009
Springer
14 years 6 months ago
2009
Springer
ATVA
2009
Springer
14 years 6 months ago
2009
Springer
This paper studies abstraction and refinement techniques in the setting of multi-valued model checking for the μ-calculus. Two dimensions of abstrace identified and studied: Abs...
ATVA
2009
Springer
14 years 6 months ago
2009
Springer
Abstract. The saturation state-space generation algorithm has demonstrated clear improvements over state-of-the-art symbolic methods for asynchronous systems. This work is motivate...