CAV
2003
Springer
14 years 5 months ago
2003
Springer
The paper considers the problem of checking abstraction between two finite-state fair discrete systems (FDS). In automata-theoretic terms this is trace inclusion between two nond...
CAV
2003
Springer
14 years 5 months ago
2003
Springer
ion and BDDs Complement SAT-based BMC in DiVer Aarti Gupta1, Malay Ganai1 , Chao Wang2, Zijiang Yang1, Pranav Ashar1 1 NEC Laboratories America, Princeton, NJ, U.S.A. 2 University ...
CAV
2003
Springer
14 years 5 months ago
2003
Springer
Many verification problems reduce to proving the validity of formulas involving both propositional connectives and domain-specific functions and predicates. This paper presents ...
CAV
2003
Springer
14 years 5 months ago
2003
Springer
We consider the problem of reasoning with linear temporal logic on truncated paths. A truncated path is a path that is finite, but not necessarily maximal. Truncated paths arise n...
CAV
2003
Springer
14 years 5 months ago
2003
Springer
Run-time monitoring of temporal properties and assertions is used for testing and as a component of execution-based model checking techniques. Traditional run-time monitoring howev...
CAV
2003
Springer
14 years 5 months ago
2003
Springer
CAV
2003
Springer
14 years 5 months ago
2003
Springer
Abstract. We present a new method for the generation of linear invariants which reduces the problem to a non-linear constraint solving problem. Our method, based on Farkas’ Lemma...
CAV
2003
Springer
14 years 5 months ago
2003
Springer
In previous work, we showed how structural information can be used to efficiently generate the state-space of asynchronous systems. Here, we apply these ideas to symbolic CTL model...
CAV
2003
Springer
14 years 5 months ago
2003
Springer
CAV
2003
Springer
14 years 5 months ago
2003
Springer
We consider the problem of synthesizing controllers for timed systems modeled using timed automata. The point of departure from earlier work is that we consider controllers that ha...