State clock logic: A decidable real-time logic

1997 ◽  
pp. 33-47 ◽  
Author(s):  
Jean-François Raskin ◽  
Pierre-Yves Schobbens
Keyword(s):  
Real Time ◽  
Time Logic

scholarly journals Model Checking via Reachability Testing for Timed Automata

1997 ◽  
Vol 4 (29) ◽  
Author(s):  
Luca Aceto ◽  
Augusto Burgueno ◽  
Kim G. Larsen
Keyword(s):  
Model Checking ◽  
Timed Automata ◽  
Reachability Problem ◽  
Liveness Properties ◽  
Time Logic ◽  
Definition Of ◽  
Reachability Testing ◽  
Time Systems ◽  
Timed Automaton ◽  
Theoretical Side

In this paper we develop an approach to model-checking for timed automata via reachability testing. As our specification formalism, we consider a dense-time logic with clocks. This logic may be used to express safety and bounded liveness properties of real-time systems. We show how to automatically synthesize, for every logical formula phi, a so-called test automaton T_phi in such a way that checking whether a system S satisfies the property phi can be reduced to a reachability question over the system obtained by making T_phi interact with S. <br />The testable logic we consider is both of practical and theoretical interest. On the practical side, we have used the logic, and the associated approach to model-checking via reachability testing it supports, in the specification and verification in Uppaal of a collision avoidance protocol. On the theoretical side, we show that the logic is powerful enough to permit the definition of characteristic properties, with respect to a timed version of<br />the ready simulation preorder, for nodes of deterministic, tau-free timed automata. This allows one to compute behavioural relations via our model-checking technique, therefore effectively reducing the problem of checking the existence of a behavioural relation among states of a timed automaton to a reachability problem.

scholarly journals Modalities for model checking: branching time logic strikes back

1987 ◽  
Vol 8 (3) ◽  
pp. 275-306 ◽  
Author(s):  
E. Allen Emerson ◽  
Chin-Laung Lei
Keyword(s):  
Model Checking ◽  
Branching Time ◽  
Time Logic
Sign in / Sign up

Export Citation Format

Share Document