FORMATS
2006
Springer
14 years 3 months ago
2006
Springer
We add freeze quantifiers to the game logic ATL in order to specify real-time objectives for games played on timed structures. We define the semantics of the resulting logic TATL b...
FORMATS
2006
Springer
14 years 3 months ago
2006
Springer
Abstract. Well-known hierarchies discriminate between the computational power of discrete time and space dynamical systems. A contrario the situation is more confused for dynamical...
FORMATS
2006
Springer
14 years 3 months ago
2006
Springer
This paper argues that basing the semantics of concurrent systems on the notions of state and state transitions is neither advisable nor necessary. The tendency to do this is deepl...
FORMATS
2006
Springer
14 years 3 months ago
2006
Springer
Abstract. Real-time systems usually encompass parts that are best described by a continuous-time model, such as physical processes under control, together with other components tha...
FORMATS
2006
Springer
14 years 3 months ago
2006
Springer
Timed and weak timed simulation relations are often used to show that operations on hybrid systems result in equivalent behavior or in conservative overapproximations. Given that s...
FORMATS
2006
Springer
14 years 3 months ago
2006
Springer
We solve some decision problems for timed automata which were raised by S. Tripakis in [Tri04] and by E. Asarin in [Asa04]. In particular, we show that one cannot decide whether a ...
FORMATS
2006
Springer
14 years 3 months ago
2006
Springer
In this paper, we consider a novel approach to the temporal logic verification problem of continuous dynamical systems. Our methodology has the distinctive feature that enables the...
FORMATS
2006
Springer
14 years 3 months ago
2006
Springer
We propose a symbolic algorithm for the analysis of the robustness of timed automata, that is the correctness of the model in presence of small drifts on the clocks or imprecision ...
FORMATS
2006
Springer
14 years 3 months ago
2006
Springer
In this paper we describe an extension of timed automata with priorities, and efficient algorithms to compute subtraction on DBMs (difference bounded matrices), needed in symbolic ...
FORMATS
2006
Springer
14 years 3 months ago
2006
Springer
Using a variant of Clariso-Cortadella's parametric method for verifying asynchronous circuits, we formally derive a set of linear constraints that ensure the correctness of so...