On discretization of delays in timed automata and digital circuits
Lecture notes in computer sciencePublished 1 January 1998
Eugène Asarin, Oded Maler, Amir Pnueli
Citations70
SJR quartileQ2
SJR score0.35
SNIP0.55
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
Abstract
In this paper we solve the following problem: "given a digital circuit composed of gates whose real-valued delays are in an integer-bounded interval, is there a way to discretize time while preserving the qualitative behavior of the circuit?" This problem is described as open in [BS94]. When "preservation of qualitative behavior" is interpreted in a strict sense, as having all original sequences of events with their original ordering we obtain the following two results: Nevertheless we show that a weaker notion of preservation, similar to that of [HMP92], allows in many cases to verify discretized circuits with δ=1 such that the verification results are valid in dense time.
Keywords
Computer Science
Theoretical Computer ScienceA theory of timed automata
6,460 Citations1994Rajeev Alur, David L. Dill
The main construction of the paper is an (PSPACE) algorithm for checking the emptiness of the language of a (nondeterministic) timed automaton, and it is proved that the universality problem and the language inclusion problem are solvable only for the deterministic automata.
Information and ComputationModel-Checking in Dense Real-Time
829 Citations1993Rajeev Alur, Costas Courcoubetis +1 more
An algorithm for model-checking, for determining the truth of a TCTL-formula with respect to a timed graph, is developed and it is argued that choosing a dense domain instead of a discrete domain to model time does not significantly blow up the complexity of the model- checking problem.
Information and ComputationSymbolic Model Checking for Real-Time Systems
823 Citations1994Thomas A. Henzinger, Xavier Nicollin +2 more
Lecture notes in computer scienceTiming assumptions and verification of finite-state concurrent systems
728 Citations1990David L. Dill
A scheme that allows timing assumptions to be incorporated into automatic proofs of arbitrary finite-state temporal properties is described, and it is conjecture that the method presented can be extended in this way.
Lecture notes in computer scienceThe tool Kronos
463 Citations1996Conrado Daws, Alfredo Olivero +2 more
Both approaches presented in this paper considerably improve Kronos performance and functionalities and improve the quality of the Kronos operating system.
Lecture notes in computer scienceWhat good are digital clocks?
276 Citations1992Thomas A. Henzinger, Zohar Manna +1 more
What can the authors conclude if a real-time system has been shown “correct” for integral observations?
Texts and monographs in computer scienceAsynchronous Circuits
169 Citations1995Janusz Brzozowski, Carl-Johan H. Seger
The asynchronous circuits is one book that the authors really recommend you to read, to get more solutions in solving this problem.
Lecture notes in computer scienceData-structures for the verification of timed automata
97 Citations1997Eugène Asarin, Marius Bozga +4 more
Numerical decision diagrams are suggested, a bdd-based data-structure for representing certain subsets of the Euclidean space, namely those encountered in verification of timed automata, because ndd's are canonical and provide for all the necessary operations needed in the verification and synthesis of timedAutomata.
Lecture notes in computer scienceTiming analysis of asynchronous circuits using timed automata
91 Citations1995Oded Maler, Amir Pnueli
These results, combined with recent results concerning the analysis and synthesis of timed automata, provide for the systematic Treatment of a large class of problems that could be treated by conventional simulation methods only in an ad-hoc fashion.
Lecture notes in computer scienceSome progress in the symbolic verification of timed automata
84 Citations1997Marius Bozga, Oded Maler +2 more
The practical difficulty of analyzing the behavior of timed automata is discussed, some results obtained using an experimental BDD-based extension of KRONOS are reported and some results outperform those obtained by previous implementations of timedAutomata verification tools.
A logic of concrete time intervals
58 Citations2002Harry R. Lewis
A finite-state model for asynchronous systems in which the time delays between the scheduling and occurrence of the events that cause state changes are constrained to fall between fixed numerical upper and lower time bounds and a branching-time temporal logic suitable for describing the temporal and logical properties of asynchronous systems.
Discretization of timed automata
43 Citations2002Aleks Göllü, Anuj Puri +1 more
Two discretizations of dense time automata are constructed which generate the same untimed language as the dense time Automata.
Hardware timing verification using KRONOS
30 Citations2002Oded Maler, Sergio Yovine
The KRONOS system, a tool for verifying real-time properties based on the model of timed-automata, is described and how it is applied to the verification of a MOS circuit under various delay assumptions is shown.
Lecture notes in computer scienceSTARI: A case study in compositional and hierarchical timing verification
30 Citations1997Serdar Taşiran, Robert K. Brayton
Using the techniques of [TAKB96], the correctness of the timing of the communication chip STARI is verified and the theory for hierarchical proofs and assume-guarantee style reasoning is developed.
Lecture notes in computer scienceFrom finite automata toward hybrid systems (Extended abstract)
16 Citations1997Alexander Rabinovich, B. A. Trakhtenbrot
This work considers two orthogonal extensions of the basic finite automaton paradigm and clarify to what degree and in what form do they preserve fundamental facts from the theory of finite automata.