Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userImproved Bounded Model Checking of Timed Automata
81
0
0.0
(
0
)
Added by
Marcello M. Bersani
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Timed Automata (TA) are a very popular modeling formalism for systems with time-sensitive properties. A common task is to verify if a network of TA satisfies a given property, usually expressed in Linear Temporal Logic (LTL), or in a subset of Timed Computation Tree Logic (TCTL). In this paper, we build upon the TACK bounded model checker for TA, which supports a signal-based semantics of TA and the richer Metric Interval Temporal Logic (MITL). TACK encodes both the TA network and property into a variant of LTL, Constraint LTL over clocks (CLTLoc). The produced CLTLoc formula can then be solved by tools such as Zot, which transforms CLTLoc properties into the input logics of Satisfiability Modulo Theories (SMT) solvers. We present a novel method that preserves TACKs encoding of MITL properties while encoding the TA network directly into the SMT solver language, making use of both the BitVector logic and the logic of real arithmetics. We also introduce several optimizations that allow us to significantly outperform the CLTLoc encoding in many practical scenarios.
rate research
Read More
This paper offers a survey of uppaalsmc, a major extension of the real-time verification tool uppaal. uppaalsmc allows for the efficient analysis of performance properties of networks of priced timed automata under a natural stochastic semantics. In particular, uppaalsmc relies on a series of extensions of the statistical model checking approach generalized to handle real-time systems and estimate undecidable problems. uppaalsmc comes together with a friendly user interface that allows a user to specify complex problems in an efficient manner as well as to get feedback in the form of probability distributions and compare probabilities to analyze performance aspects of systems. The focus of the survey is on the evolution of the tool - including modeling and specification formalisms as well as techniques applied - together with applications of the tool to case studies.
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.
We solve some decision problems for timed automata which were recently raised by S. Tripakis in [ Folk Theorems on the Determinization and Minimization of Timed Automata, in the Proceedings of the International Workshop FORMATS2003, LNCS, Volume 2791, p. 182-188, 2004 ] and by E. Asarin in [ Challenges in Timed Languages, From Applied Theory to Basic Theory, Bulletin of the EATCS, Volume 83, p. 106-120, 2004 ]. In particular, we show that one cannot decide whether a given timed automaton is determinizable or whether the complement of a timed regular language is timed regular. We show that the problem of the minimization of the number of clocks of a timed automaton is undecidable. It is also undecidable whether the shuffle of two timed regular languages is timed regular. We show that in the case of timed Buchi automata accepting infinite timed words some of these problems are Pi^1_1-hard, hence highly undecidable (located beyond the arithmetical hierarchy).
Automata expressiveness is an essential feature in understanding which of the formalisms available should be chosen for modelling a particular problem. Probabilistic and stochastic automata are suitable for modelling systems exhibiting probabilistic behavior and their expressiveness has been studied relative to non-probabilistic transition systems and Markov chains. In this paper, we consider previous formalisms of Timed, Probabilistic and Stochastic Timed Automata, we present our new model of Timed Automata with Polynomial Delay, we introduce a measure of expressiveness for automata we call trace expressiveness and we characterize the expressiveness of these models relative to each other under this new measure.
We study complexity of the model-checking problems for LTL with registers (also known as freeze LTL) and for first-order logic with data equality tests over one-counter automata. We consider several classes of one-counter automata (mainly deterministic vs. nondeterministic) and several logical fragments (restriction on the number of registers or variables and on the use of propositional variables for control locations). The logics have the ability to store a counter value and to test it later against the current counter value. We show that model checking over deterministic one-counter automata is PSPACE-complete with infinite and finite accepting runs. By constrast, we prove that model checking freeze LTL in which the until operator is restricted to the eventually operator over nondeterministic one-counter automata is undecidable even if only one register is used and with no propositional variable. As a corollary of our proof, this also holds for first-order logic with data equality tests restricted to two variables. This makes a difference with the facts that several verification problems for one-counter automata are known to be decidable with relatively low complexity, and that finitary satisfiability for the two logics are decidable. Our results pave the way for model-checking memoryful (linear-time) logics over other classes of operational models, such as reversal-bounded counter machines.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
