Undecidability of universality for timed automata with minimal resources by Adams, S, Ouaknine, J, Worrell, J

“…A fundamental limit to the algorithmic analysis of timed automata, however, results from the undecidability of the universality problem: does a given timed automaton accept every timed word? As a result, much research has focussed on attempting to circumvent this difficulty, often by restricting the class of automata under consideration, or by altering their semantics. …”

Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata by Jovanovic, A, Kwiatkowska, M, Norman, G, Peyras, Q

“…In this paper we consider the problem of computing the optimal (minimum or maximum) expected time to reach a target and the synthesis of an optimal controller for a probabilistic timed automaton (PTA). Although this problem admits solutions that employ the digital clocks abstraction or statistical model checking, symbolic methods based on zones and priced zones fail due to the difficulty of incorporating probabilistic branching in the context of dense time. …”

Expected Reachability-Time Games. by Forejt, V, Kwiatkowska, M, Norman, G, Trivedi, A

“…In an expected reachability-time game (ERTG) two players, Min and Max, move a token along the transitions of a probabilistic timed automaton, so as to minimise and maximise, respectively, the expected time to reach a target. …”

Parametric updates in parametric timed automata by Étienne André, Didier Lime, Mathias Ramparison

“…We focus here on the EF-emptiness problem: "is the set of parameter valuations for which some given location is reachable in the instantiated timed automaton empty?". This problem is well-known to be undecidable for PTAs, and so it is for our extension. …”
Get full text

Completeness of Lyapunov Abstraction by Rafael Wisniewski, Christoffer Sloth

“…Our construction gives rise to a combinatorial object - a timed automaton. We examine sound and complete abstractions. …”
Get full text

Time−Bounded Verification of CTMCs Against Real−Time Specifications by Chen, T, Diciolla, M, Kwiatkowska, M, Mereacre, A

“…In this paper we study time-bounded verification of a finite continuous-timeMarkov chain (CTMC) C against a real-time specification, provided either as a metric temporal logic (MTL) property 'φ', or as a timed automaton (TA) A. The key question is: what is the probability of the set of timed paths of C that satisfy 'φ' (or are accepted by A) over a time interval of fixed, bounded length? …”

Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications by Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre

“…We study the verification of a finite continuous-time Markov chain (CTMC) C against a linear real-time specification given as a deterministic timed automaton (DTA) A with finite or Muller acceptance conditions. …”
Get full text

Optimal controller synthesis for timed systems by Damien Busatto-Gaston, Benjamin Monmege, Pierre-Alain Reynier

“…Weighted timed games are zero-sum games played by two players on a timed automaton equipped with weights, where one player wants to minimise the cumulative weight while reaching a target. …”
Get full text

Universality Analysis for One-Clock Timed Automata by Abdulla, P, Deneux, J, Ouaknine, J, Quaas, K, Worrell, J

“…This paper is concerned with the universality problem for timed automata: given a timed automaton A, does A accept all timed words? Alur and Dill have shown that the universality problem is undecidable if A has two clocks, but they left open the status of the problem when A has a single clock. …”

On parametric timed automata and one-counter machines by Ouaknine, J, Bundala, D

“…s decision procedure for one parametric clock from nonelementary to 2NEXP; (ii) to show decidability for two parametric clocks provided the timed automaton uses only a single parameter; (iiii) to show decidability for various resulting classes of parametric one-counter machines; and (iv) to show decidability of reachability for the simple programs of Ibarra et al. in the presence of a single parameter. …”

A Reaction-Diffusion Heart Model for the Closed-Loop Evaluation of Heart-Pacemaker Interaction by Niccolo Biasi, Paolo Seghetti, Matteo Mercati, Alessandro Tognetti

“…We modelled the pacemaker as a timed automaton, deployed on an Arduino 2 board. The Arduino and the workstation communicate through a PCI acquisition board. …”
Get full text

Timed Parity Games: Complexity and Robustness by Krishnendu Chatterjee, Thomas A. Henzinger, Vinayak S. Prabhu

“…For both kinds of robust strategies, we present efficient reductions to standard timed automaton games. These reductions provide algorithms for the synthesis of robust real-time controllers.…”
Get full text

Design and model checking of timed automata oriented architecture for Internet of thing by Guang Chen, Tonghai Jiang, Meng Wang, Xinyu Tang, Wenfei Ji

“…This article discusses the method and practice of time automaton modeling and model checking for the architecture of the Internet of thing system from the state and time dimensions. …”
Get full text