Abstract:
One clock alternating timed automata OCATA have been recently introduced as natural extension of (one clock) timed automata to express the semantics of MTL (Ouaknine, Worrell 2005). We consider the application of OCATA to problem of model-checking MITL formulas (a syntactic fragment of MTL) against timed automata. We introduce a new semantics for OCATA where, intuitively, clock valuations are intervals instead of single real values. Thanks to this new semantics, we show that we can bound the number of clock copies that are necessary to allow an OCATA to recognise the models of an MITL formula. Equipped with this technique, we propose a new algorithm to translate an MITL formula into a timed automaton, and we sketch several ideas to define new model checking algorithms for MITL.

Abstract:
One clock alternating timed automata (OCATA) have been introduced as natural extension of (one clock) timed automata to express the semantics of MTL. In this paper, we consider the application of OCATA to the problems of model-checking and satisfiability for MITL (a syntactic fragment of MTL), interpreted over infinite words. Our approach is based on the interval semantics (recently introduced in [BEG13] in the case of finite words) extended to infinite words. We propose region-based and zone-based algorithms, based on this semantics, for MITL model-checking and satisfiability. We report on the performance of a prototype tool implementing those algorithms.

Abstract:
In this paper, the problem of checking a timed automaton for a Duration Calculus formula of the form Temporal Duration Property is addressed. It is shown that Temporal Duration Properties are in the class of discretisable real-time properties of Timed Automata, and an algorithm is given to solve the problem based on linear programming techniques and the depth-first search method in the integral region graph of the automaton. The complexity of the algorithm is in the same class as that of the solution of the reachability problem of timed automata.

Abstract:
The parameter synthesis problem for timed automata is undecidable in general even for very simple reachability properties. In this paper we introduce restrictions on parameter valuations under which the parameter synthesis problem is decidable for LTL properties. The proposed problem could be solved using an explicit enumeration of all possible parameter valuations. However, we introduce a symbolic zone-based method for synthesising bounded integer parameters of parametric timed automata with an LTL specification. Our method extends the ideas of the standard automata-based approach to LTL model checking of timed automata. Our solution employs constrained parametric difference bound matrices and a suitable notion of extrapolation.

Abstract:
Probabilistic timed automata are an extension of timed automata with discrete probability distributions. We consider model-checking algorithms for the subclasses of probabilistic timed automata which have one or two clocks. Firstly, we show that PCTL probabilistic model-checking problems (such as determining whether a set of target states can be reached with probability at least 0.99 regardless of how nondeterminism is resolved) are PTIME-complete for one-clock probabilistic timed automata, and are EXPTIME-complete for probabilistic timed automata with two clocks. Secondly, we show that, for one-clock probabilistic timed automata, the model-checking problem for the probabilistic timed temporal logic PCTL is EXPTIME-complete. However, the model-checking problem for the subclass of PCTL which does not permit both punctual timing bounds, which require the occurrence of an event at an exact time point, and comparisons with probability bounds other than 0 or 1, is PTIME-complete for one-clock probabilistic timed automata.

Abstract:
It is proved in this paper that checking a timed automaton M with respect to a linear duration property D can be done by investigating only the integral timed states of M. An equivalence relation is introduced in this paper to divide the infinite number of integral timed states into finite number of equivalence classes. Based on this, a method is proposed for checking whether M satisfies D. In some cases, the number of equivalence classes is too large for a computer to manipulate. A technique for reducing the search-space for checking linear duration property is also described. This technique is more suitable for the case in this paper than those in the literature because most of those techniques are designed for reachability analysis.

Abstract:
We consider the model of priced (a.k.a. weighted) timed automata, an extension of timed automata with cost information on both locations and transitions, and we study various model-checking problems for that model based on extensions of classical temporal logics with cost constraints on modalities. We prove that, under the assumption that the model has only one clock, model-checking this class of models against the logic WCTL, CTL with cost-constrained modalities, is PSPACE-complete (while it has been shown undecidable as soon as the model has three clocks). We also prove that model-checking WMTL, LTL with cost-constrained modalities, is decidable only if there is a single clock in the model and a single stopwatch cost variable (i.e., whose slopes lie in {0,1}).

Abstract:
This paper offers a natural stochastic semantics of Networks of Priced Timed Automata (NPTA) based on races between components. The semantics provides the basis for satisfaction of probabilistic Weighted CTL properties (PWCTL), conservatively extending the classical satisfaction of timed automata with respect to TCTL. In particular the extension allows for hard real-time properties of timed automata expressible in TCTL to be refined by performance properties, e.g. in terms of probabilistic guarantees of time- and cost-bounded properties. A second contribution of the paper is the application of Statistical Model Checking (SMC) to efficiently estimate the correctness of non-nested PWCTL model checking problems with a desired level of confidence, based on a number of independent runs of the NPTA. In addition to applying classical SMC algorithms, we also offer an extension that allows to efficiently compare performance properties of NPTAs in a parametric setting. The third contribution is an efficient tool implementation of our result and applications to several case studies.

Abstract:
Parametric timed automata extend timed automata (Alur and Dill, 1991) in that they allow the specification of parametric bounds on the clock values. Since their introduction in 1993 by Alur, Henzinger, and Vardi, it is known that the emptiness problem for parametric timed automata with one clock is decidable, whereas it is undecidable if the automaton uses three or more parametric clocks. The problem is open for parametric timed automata with two parametric clocks. Metric temporal logic, MTL for short, is a widely used specification language for real-time systems. MTL-model checking of timed automata is decidable, no matter how many clocks are used in the timed automaton. In this paper, we prove that MTL-model checking for parametric timed automata is undecidable, even if the automaton uses only one clock and one parameter and is deterministic.

Abstract:
This paper presents the first model-checking algorithm for an expressive modal mu-calculus over timed automata, $L^{\mathit{rel}, \mathit{af}}_{\nu,\mu}$, and reports performance results for an implementation. This mu-calculus contains extended time-modality operators and can express all of TCTL. Our algorithmic approach uses an "on-the-fly" strategy based on proof search as a means of ensuring high performance for both positive and negative answers to model-checking questions. In particular, a set of proof rules for solving model-checking problems are given and proved sound and complete; we encode our algorithm in these proof rules and model-check a property by constructing a proof (or showing none exists) using these rules. One noteworthy aspect of our technique is that we show that verification performance can be improved with \emph{derived rules}, whose correctness can be inferred from the more primitive rules on which they are based. In this paper, we give the basic proof rules underlying our method, describe derived proof rules to improve performance, and compare our implementation of this model checker to the UPPAAL tool.