This chapter is to provide a tutorial and pointers to results and related work on timed automata with a focus on semantical and algorithmic aspects of verification tools. We prese...
We consider several questions related to the use of digitization techniques for timed automata. These very successful techniques reduce dense-time language inclusion problems to d...
In a former paper, we defined a new semantics for timed automata, the Almost ASAP semantics, which is parameterized by ∆ to cope with the reaction delay of the controller. We sh...
Martin De Wulf, Laurent Doyen, Nicolas Markey, Jea...
A Time Action Lock is a state of a Real-time system at which neither time can progress nor an action can occur. Time Action Locks are often seen as signs of errors in the model or ...
Abstract. This paper is concerned with the language inclusion problem for timed automata: given timed automata A and B, is every word accepted by B also accepted by A? Alur and Dil...
Abstract. We examine to what extent implementation of timed automata can be achieved using the standard semantics and appropriate modeling, instead of introducing new semantics. We...
Recently we have proposed the ”almost ASAP” semantics as an alternative semantics for timed automata. This semantics is useful when modeling real-time controllers : control str...
In this paper we show how we can translate Web Services described by WS-CDL into a timed automata orchestration, and more specifically we are interested in Web services with time ...
In this paper, we present the features of Romeo, a Time Petri Net (TPN) analyzer. The tool Romeo allows state space computation of TPN and on-the-fly model-checking of reachabilit...
Guillaume Gardey, Didier Lime, Morgan Magnin, Oliv...
— Schedule synthesis based on reachability analysis of timed automata has received attention in the last few years. The main strength of this approach is that the expressiveness ...
Gerd Behrmann, Ed Brinksma, Martijn Hendriks, Ange...