scholarly journals Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata

2021 ◽  
pp. 311-329 ◽  
Author(s):  
Étienne André ◽  
Jaime Arias ◽  
Laure Petrucci ◽  
Jaco van de Pol
Keyword(s):  
Timed Automata ◽  
Graph Searching ◽  
Successful Termination ◽  
All Solutions ◽  
Parameter Synthesis ◽  
Pruning Algorithms ◽  
Timed Automaton ◽  
Cycle Detection

AbstractWe study semi-algorithms to synthesise the constraints under which a Parametric Timed Automaton satisfies some liveness requirement. The algorithms traverse a possibly infinite parametric zone graph, searching for accepting cycles. We provide new search and pruning algorithms, leading to successful termination for many examples. We demonstrate the success and efficiency of these algorithms on a benchmark. We also illustrate parameter synthesis for the classical Bounded Retransmission Protocol. Finally, we introduce a new notion of completeness in the limit, to investigate if an algorithm enumerates all solutions.

MODELING AND ANALYSIS OF REAL-TIME SYSTEMS WITH MUTEX COMPONENTS

2012 ◽  
Vol 23 (04) ◽  
pp. 831-851 ◽  
Author(s):  
GUOQIANG LI ◽  
XIAOJUAN CAI ◽  
SHOJI YUEN
Keyword(s):  
Real Time ◽  
Timed Automata ◽  
Expressive Power ◽  
Behavioral Model ◽  
Parallel Composition ◽  
Real Time Systems ◽  
Modeling And Analysis ◽  
Compositional System ◽  
Time Systems ◽  
Timed Automaton

Timed automata are commonly recognized as a formal behavioral model for real-time systems. For compositional system design, parallel composition of timed automata as proposed by Larsen et al. [22] is useful. Although parallel composition provides a general method for system construction, in the low level behavior, components often behave sequentially by passing control via communication. This paper proposes a behavioral model, named controller automata, to combine timed automata by focusing on the control passing between components. In a controller automaton, to each state a timed automaton is assigned. A timed automaton at a state may be preempted by the control passing to another state by a global labeled transition. A controller automaton properly extends the expressive power because of the stack, but this can make the reachability problem undecidable. Given a strict partial order over states, we show that this problem can be avoided and a controller automaton can be faithfully translated into a timed automaton.

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.

On clock-aware LTL parameter synthesis of timed automata

2018 ◽  
Vol 99 ◽  
pp. 114-142
Author(s):  
Peter Bezděk ◽  
Nikola Beneš ◽  
Ivana Černá ◽  
Jiří Barnat
Keyword(s):  
Timed Automata ◽  
Parameter Synthesis

scholarly journals Transfer of Temporal Logic Formulas in Reinforcement Learning

2019 ◽  
Author(s):  
Zhe Xu ◽  
Ufuk Topcu
Keyword(s):  
Reinforcement Learning ◽  
Temporal Logic ◽  
Timed Automata ◽  
Disjunctive Normal Form ◽  
Transfer Of Knowledge ◽  
Extended State ◽  
Target Task ◽  
Order Of Magnitude ◽  
High Level ◽  
Timed Automaton

Transferring high-level knowledge from a source task to a target task is an effective way to expedite reinforcement learning (RL). For example, propositional logic and first-order logic have been used as representations of such knowledge. We study the transfer of knowledge between tasks in which the timing of the events matters. We call such tasks temporal tasks. We concretize similarity between temporal tasks through a notion of logical transferability, and develop a transfer learning approach between different yet similar temporal tasks. We first propose an inference technique to extract metric interval temporal logic (MITL) formulas in sequential disjunctive normal form from labeled trajectories collected in RL of the two tasks. If logical transferability is identified through this inference, we construct a timed automaton for each sequential conjunctive subformula of the inferred MITL formulas from both tasks. We perform RL on the extended state which includes the locations and clock valuations of the timed automata for the source task. We then establish mappings between the corresponding components (clocks, locations, etc.) of the timed automata from the two tasks, and transfer the extended Q-functions based on the established mappings. Finally, we perform RL on the extended state for the target task, starting with the transferred extended Q-functions. Our implementation results show, depending on how similar the source task and the target task are, that the sampling efficiency for the target task can be improved by up to one order of magnitude by performing RL in the extended state space, and further improved by up to another order of magnitude using the transferred extended Q-functions.

scholarly journals Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata

2021 ◽  
Author(s):  
Jaco van de Pol ◽  
Laure Petrucci ◽  
Jaime Arias ◽  
Étienne André
Keyword(s):  
Timed Automata ◽  
Cycle Detection

scholarly journals From Timed Automata to Logic - and Back

1995 ◽  
Vol 2 (2) ◽  
Author(s):  
Francois Laroussinie ◽  
Kim G. Larsen ◽  
Carsten Weise
Keyword(s):  
Model Checking ◽  
Real Time ◽  
Timed Automata ◽  
Finite Automata ◽  
Automatic Verification ◽  
Satisfiability Problem ◽  
Timed Automaton

One of the most successful techniques for automatic verification is that<br />of model checking. For finite automata there exist since long extremely<br />efficient model-checking algorithms, and in the last few years these algorithms have been made applicable to the verification of real-time automata using the region-techniques of Alur and Dill.<br />In this paper, we continue this transfer of existing techniques from the<br />setting of finite (untimed) automata to that of timed automata. In particular, a timed logic L is put forward, which is sufficiently expressive that we for any timed automaton may construct a single characteristic L formula uniquely characterizing the automaton up to timed bisimilarity. Also, we prove decidability of the satisfiability problem for L with respect to given bounds on the number of clocks and constants of the timed automata to be constructed. None of these results have as yet been succesfully accounted for in the presence of time.

scholarly journals Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction*

2021 ◽  
Vol 178 (1-2) ◽  
pp. 31-57
Author(s):  
Franck Cassez ◽  
Peter Gjøl Jensen ◽  
Kim Guldstrand Larsen
Keyword(s):  
Real Time ◽  
State Of The Art ◽  
Timed Automata ◽  
Robustness Analysis ◽  
Hybrid Automata ◽  
Timed Systems ◽  
Current State ◽  
Parameter Synthesis ◽  
Series Of Experiments ◽  
Time Systems

We address the safety verification and synthesis problems for real-time systems. We introduce real-time programs that are made of instructions that can perform assignments to discrete and real-valued variables. They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata. We propose a semi-algorithm using refinement of trace abstractions to solve both the reachability verification problem and the parameter synthesis problem for real-time programs. All of the algorithms proposed have been implemented and we have conducted a series of experiments, comparing the performance of our new approach to state-of-the-art tools in classical reachability, robustness analysis and parameter synthesis for timed systems. We show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools.

Sign in / Sign up

Export Citation Format

Share Document