FORMATS
2004
Springer
14 years 3 months ago
2004
Springer
Davies and Wakerly show that Byzantine fault tolerance can be achieved by a cascade of broadcasts and middle value select functions. We present an extension of the Davies and Waker...
FORMATS
2004
Springer
14 years 3 months ago
2004
Springer
This paper presents assume-guarantee style substitutivity results for the recently published timed I/O automaton modeling framework. These results are useful for decomposing verifi...
FORMATS
2004
Springer
14 years 3 months ago
2004
Springer
The hierarchy of untimed equivalences is well understood for action-based systems. This is not the case for timed systems, where it is, for example, possible to detect concurrency ...
FORMATS
2004
Springer
14 years 3 months ago
2004
Springer
We discuss the modeling and verification of real-time systems using the SAL model checker. A new modeling framework based on event calendars enables dense timed systems to be descr...
FORMATS
2004
Springer
14 years 3 months ago
2004
Springer
Abstract. In this paper we report a new SAT solver for difference logic, a propositional logic enriched with timing constraints. The main novelty of our solver is a tighter integra...
FORMATS
2004
Springer
14 years 4 months ago
2004
Springer
Abstract. We describe OBDD-based symbolic model checking algorithms for simply-timed systems, i.e. finite state graphs where transitions carry a duration. These durations can be a...
FORMATS
2004
Springer
14 years 4 months ago
2004
Springer
Abstract. In this paper we introduce a variant of temporal logic tailored for specifying desired properties of continuous signals. The logic is based on a bounded subset of the rea...
FORMATS
2004
Springer
14 years 4 months ago
2004
Springer
Abstract. We extend Angluin’s algorithm for on-line learning of regular languages to the setting of timed systems. We consider systems that can be described by a class of determi...
FORMATS
2004
Springer
14 years 4 months ago
2004
Springer
FORMATS
2004
Springer
14 years 4 months ago
2004
Springer
Probabilistic timed automata are timed automata extended with discrete probability distributions, and can be used to model timed randomised protocols or faulttolerant systems. We ...