A theory of timed automata, Rajeev Alur, David L. Dill
https://www.sciencedirect.com/science/article/pii/0304397594900108
References
[1] R. Alur, C. Courcoubetis, D. Dill, Model-checking for real-time systems Proc. 5th IEEE Symp. on Logic in Computer Science (1990), pp. 414-425
[2] R. Alur, C. Courcoubetis, D. Dill, Model-checking for probabilistic real-time systems Automata, Languages and Programming: Proc. 18th ICALP, Vol. 510, Springer, Berlin (1991), pp. 115-136
[3] R. Alur, C. Courcoubetis, D. Dill, Verifying automata specifications of probabilistic real-time systemsm Proc. REX Workshop “Real-Time: Theory in Practice”, Vol. 600, Springer, Berlin (1991), pp. 28-44
[4] R. Alur, T. Feder, T. Henzinger, The benefits of relaxing punctuality, Proc. 10th ACM Symp. on Principles of Distributed Computing (1991), pp. 139-152
[5] R. Alur, T. Henzinger, A really temporal logic, Proc. 30th IEEE Symp. on Foundations of Computer Science (1989), pp. 164-169
[6] A. Bernstein, P. Harter, Proving real-time properties of programs with temporal logic, Proc. 8th ACM Symp. on Operating System Principles (1981), pp. 164-176
[7] R. Büchi, On a decision method in restricted second-order arithmetic, Proc. Internat. Cong. on Logic, Methodology, and Philosophy of Science 1960, Stanford University Press, Stanford (1962), pp. 1-12
[8] J. Burch, E. Clarke, D. Dill, L. Hwang, K.L. McMillan, Symbolic model checking: 1020 states and beyond, Inform. and Comput., 98 (2) (1992), pp. 142-170
https://pdf.sciencedirectassets.com/272575/1-s2.0-S0890540100X02118/1-s2.0-089054019290017A/main.pdf?X-Amz-Security-Token=IQoJb3JpZ2luX2VjECAaCXVzLWVhc3QtMSJHMEUCIC9ZMWnmYLYvjy3dGPgPn4O4MprT41p4N3pwqabbEJQlAiEAikk%2BSJUTO9yIRVQJZM8lB37jXuFrVvCKzerhs1cEnscqsgUIORAFGgwwNTkwMDM1NDY4NjUiDJX7C0cIcNOLUXT61CqPBcFXnsLOQF5KBHl01kcu%2FcXIvT9116muu2M6cwj9L8MsWkHb5u06G2ppDKw%2BnuASj%2F6p%2B%2BC0Q2qdGaAemh7TPJJgJsgJb%2B%2FnRCFfLgPMbzb3U1SvyuUKttPuHjVLtaCD0UE%2F07V5uoKCzgV%2Bg0kZ9nedc%2FnZjVJsJhgEj2hC%2B7YsfQ8pNb9vydyFSfC8IJc6tFp%2BkUr1sL9Zphcf2Vpnr39nV8JzdZlnAMMvrZJMEkNtjIpWRxdlA7yZ4OYM%2F6u%2FCmKQi373rXhN7CDXEz519jloYghrPWej7XakkctRM6n%2F1U%2FaXhPQGWpxXvWfwCv49FrZRiDqek3zFgQxgEMtBV%2BS9vUmfzeR9sSGLsdS7XtMqJMpNOW7rlSQ4RHQ1f94axfqNnTxpzPS1rAT9iEeHjMqBM8H0WJ09IBAAFZle7EEt674yFNOBtG%2F3s5ZQSozZFvxxCWamATdGW%2B8QeV8vxx3RvhvsgHXiP9nqBW%2BuWztSC6gCKsPKQppl5XGX%2FT%2BZ7krKlr0v6W3MO0KI3tRG%2FX%2FO%2Bv4rdqzqeUdW9CMHuZ2z2kTi1aj4b8sb7NeNEI8g9oEcFF1Z%2FJr2BBv%2FconBb4VbsnhoaS617tjl8AW7MFKfY6xGPx9Nqg4QfbfpqXNZtyH5z1rM74tRsB3yneBSRLQ5dwMhhfsOn7s8rRiUux4EkdOoNU2llyj3txdbRryBkxf33j8Kv10%2BPYRvaia1gXAzvKiDPD7AQwZDF3Nzfxcqz8air8mm0FuL871rjt2rK9j%2FZRzqGWegS7OrT6S7R3tsfDjqlZ4rE1UqTjevYAdQVvE0%2BAOSySvYr%2FcZ9qHhzF8BfEZWWxcwWz70rTA9Q303Q%2FHTi33DuXLPfI%2FGiUwzqLWwwY6sQE0TuF7kHMtW7wSQcTkUoovuaEfRKEbMzwqvtgxvAT9WnWTW64CHn6CCEQa52KoijZQs0Hl1wVrUTmQGnl83Mu8m9d45HP6seIZ6K4vJCIrv9pO4SlbFNgHAO3UNw83spWwHI4ZtU7DNBg2FqS3Qd9%2BbzmQJdIN%2BCUEH4fZ%2F6sSKcVaLsP%2BojT103BWZ0xj7%2BgbMiMnCNMEVcTnG5qq5p46X0alaCHcT4L3hBct3d%2BnM0Q%3D&X-Amz-Algorithm=AWS4-HMAC-SHA256&X-Amz-Date=20250715T003622Z&X-Amz-SignedHeaders=host&X-Amz-Expires=300&X-Amz-Credential=ASIAQ3PHCVTY7BOKLNXR%2F20250715%2Fus-east-1%2Fs3%2Faws4_request&X-Amz-Signature=3c1a6d51db3e3f459a0ec424cdeb85e8227a7c91fdc23c9f417664f28c329fb7&hash=a9ec0ea9d958f3ef382e3cbc68547df409a6b1bb35765631b95ba3f6760b9de7&host=68042c943591013ac2b2430a89b270f6af2c76d8dfd086a07176afe7c76c2c61&pii=089054019290017A&tid=spdf-c6ffc1d7-1857-446c-a537-50ba1e167393&sid=89ca8935431f944a4b5afa613eb4d9a07649gxrqa&type=client&tsoh=d3d3LnNjaWVuY2VkaXJlY3QuY29t&rh=d3d3LnNjaWVuY2VkaXJlY3QuY29t&ua=05125851015b520858&rr=95f52f65288df5e9&cc=jp
[9] K. Čerāns, Decidability of bisimulation equivalence for parallel timer processes, in Proc. 4th Workshop on Computer-aided Verification, Lecture Notes in Computer Science (to appear).
[10] Y. Choueka, Theories of automata on ω-tapes: a simplified approach, J. Comput. System Sci., 8 (1974), pp. 117-141
https://pdf.sciencedirectassets.com/272574/1-s2.0-S0022000074X80510/1-s2.0-S0022000074800516/main.pdf?X-Amz-Security-Token=IQoJb3JpZ2luX2VjECAaCXVzLWVhc3QtMSJHMEUCIQDedzYdSwoaTspqoAr7AKOnnMLWWxazCEQAJz48I7EyigIgBbkx3vcuq3VBWazuBUw8KKg4JwElZG%2BDL3aKPTSpXJ0qsgUIOBAFGgwwNTkwMDM1NDY4NjUiDJtaiZQo%2FvsrmDIS%2FiqPBZAxUhRdUAxXPHuJ%2BPI4hxdvVdrJivvY3me0%2BEGsLBujIaityAeGwJ4%2BvcrXJl%2BVhW9g6HFMgadL3j7%2FNMAhdRNHCIIuq7U0RZ%2BZKLlGwwmi7cuzHfTuHjwEYi7KABGR9XLFqFsd9ViF8MPWZVxRl1nWB6O5nLX6qU2s6ENqq%2Bi11EnYGsl1i3RQhthWLabIGmkjXfe1zAdPhkxfetrsroNnDjG0k7UqpJ2zkHJCAfzWw8JXSCVjKN4tcW4I4EV7OM%2BU9lROZ8DddRzaWrKtIKOH%2FN7R5Zc3CQm3EEbSYRClokVdU5Mllu1ty5uZV7Qac5sJ%2FerQm39cCb3mZM2kZKhDcff%2BcfEkEEJpl0wZAr5fzsJTZu%2Bh3JUtLc8kg9Sl9azlXeo17OTQOJl%2FFw7%2B%2F7QU%2Fy3h%2BysLP8nmlA7f%2FOl%2F4rjttwZbuu1VARUmS7aFigu8FRBn0KmHnD2IHES7%2BH6pDyiQ987bNlaapmpHtlbeCh0l9mTQMgWVtaTnttldrLU4evLCft3Q4FEbG2Cge8mnvTRzZ9hg5R73pvrPaQCvgI8t0qEr1VN88ePW1RGuEk6LHgPm7zZneVq9ckaGLbJbdJkU%2F339WH4%2FkOZnUpFcTARfIp8H1H%2Fhaw5BPbBiCC2E7nGfFdyQbdPFte4KVldyg0V6DGUuXz0dBgFOYxh%2FBHSxWHQRV25qXop0Zn2RXVedtvaZQ788VPq9robTuAvsl%2BdtDWVi%2BcaJ2w01JoRI3VudLrB95MK33xPhnyUiaEe7JiYD%2BbC99mINN3%2FDN1V3fUvO09LwSWeiSL1f5hMPQ1ycC6h4YHqw7ec3tJR52VlgrDYuy3aHIV0r4Pbi5LJq41utJcvsvt9RDj%2Bt2KEw6qHWwwY6sQHus74z5zRvLSSsu6gqJWZYqSzOr57UI0KYQsQH7RDc8Hh8E3pGHoAFoNldZRt4XaaIkwcMLSElmNeIfuppEyBn2B5YtdfIP69vvCUBZDSknCNfbPmHChXLEGEAwJb91yW4hYA4pFIHCnGGiYx%2Bo48wOQRbMGFLLNLzRz%2FTsHMuiMCjB94b%2B8lWW%2BcsyFGkQZNbbvLL2IKMw5vzPxc9saPWomh%2FyH7qCe%2BHffyaXFu73aA%3D&X-Amz-Algorithm=AWS4-HMAC-SHA256&X-Amz-Date=20250715T004140Z&X-Amz-SignedHeaders=host&X-Amz-Expires=300&X-Amz-Credential=ASIAQ3PHCVTYYTDXJQZ3%2F20250715%2Fus-east-1%2Fs3%2Faws4_request&X-Amz-Signature=379c8da9c196efa86a6c45e73f76d91bcefbec15405d1b67cebf8f84d3ae8ead&hash=a16ccd81f87c291fea7b09f99e59a3e72834b0c16f97e6d4064631e1999e76a1&host=68042c943591013ac2b2430a89b270f6af2c76d8dfd086a07176afe7c76c2c61&pii=S0022000074800516&tid=spdf-63122ea7-9372-49c0-996e-90834d437d83&sid=89ca8935431f944a4b5afa613eb4d9a07649gxrqa&type=client&tsoh=d3d3LnNjaWVuY2VkaXJlY3QuY29t&rh=d3d3LnNjaWVuY2VkaXJlY3QuY29t&ua=05125851015b53595c&rr=95f537295d3cf5e9&cc=jp
[11] E. Clarke, I. Draghicescu, R. Kurshan, A unified approach for showing language containment and equivalence between various types of ω-automata, Tech. Report, Carnegie Mellon University (1989)
Google Scholar
[12]
E. Clarke, E.A. Emerson, A.P. Sistla
Automatic verification of finite-state concurrent systems using temporal-logic specifications
ACM Trans. Programming Languages and Systems, 8 (2) (1986), pp. 244-263
View in ScopusGoogle Scholar
[13]
C. Courcoubetis, M. Yannakakis
Minimum and maximum delay problems in real-time systems
Proc. 3rd Workshop on Computer-Aided Verification, Vol. 575, Springer, Berlin (1991), pp. 399-409
Lecture Notes in Computer Science
Google Scholar
[14]
D. Dill
Timing assumptions and verification of finite-state concurrent systems
J. Sifakis (Ed.), Automatic Verification Methods for Finite State Systems, Vol. 407, Springer, Berlin (1989), pp. 197-212
Lecture Notes in Computer Science
Google Scholar
[15]
D. Dill
Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits
MIT Press, Cambridge, MA (1989)
Google Scholar
[16]
D. Dill, H. Wong-Toi
Synthesizing processes and schedulers from temporal specifications
Proc. 2nd Workshop on Computer-Aided Verification, Vol. 531, Springer, Berlin (1990), pp. 272-281
Lecture Notes in Computer Science
Google Scholar
[17]
E.A. Emerson, E.M. Clarke
Using branching-time temporal logic to synthesize synchronization skeletons
Sci. Comput. Programming, 2 (1982), pp. 241-266
View PDF
View articleView in ScopusGoogle Scholar
[18]
E.A. Emerson, A. Mok, A.P. Sistla, J. Srinivasan
Quantitative temporal reasoning
Proc. 2nd Workshop on Computer-Aided Verification, Vol. 531, Springer, Berlin (1990), pp. 136-145
Lecture Notes in Computer Science
Google Scholar
[19]
P. Godefroid, P. Wolper
A partial approach to model-checking
Proc. 6th IEEE Symp. on Logic in Computer Science (1991), pp. 406-415
View in ScopusGoogle Scholar
[20]
E. Harel, O. Lichtenstein, A. Pnueli
Explicit-clock temporal logic
Proc. 5th IEEE Symp. on Logic in Computer Science (1990), pp. 402-413
View in ScopusGoogle Scholar
[21]
D. Harel, A. Pnueli, J. Stavi
Propositional dynamic logic of regular programs
J. Comput. System Sci., 26 (1983), pp. 222-243
View PDF
View articleView in ScopusGoogle Scholar
[22]
T. Henzinger, Z. Manna, A. Pnueli
Temporal proof methodologies for real-time systems
Proc. 18th ACM Symp. on Principles of Programming Languages (1991), pp. 353-366
View in ScopusGoogle Scholar
[23]
C. Hoare
Communicating sequential processes
Comm. ACM, 21 (1978), pp. 666-677
View in ScopusGoogle Scholar
[24]
J. Hopcroft, J. Ullman
Introduction to Automata Theory, Languages, and Computation
Addison-Wesley, Reading, MA (1979)
Google Scholar
[25]
F. Jahanian, A. Mok
Safety analysis of timing properties in real-time systems
IEEE Trans. Software Engrg., SE-12 (1986), pp. 890-904
View in ScopusGoogle Scholar
[26]
F. Jahanian, A. Mok
A graph-theoretic approach for timing analysis and its implementation
IEEE Trans. Comput., C-36 (1987), pp. 961-975
View in ScopusGoogle Scholar
[27]
R. Koymans
Specifying real-time properties with metric temporal logic
J. Real-time Systems, 2 (1990), pp. 255-299
View in ScopusGoogle Scholar
[28]
R. Kurshan
Complementing deterministic Büchi automata in polynomial time
J. Comput. System Sci., 35 (1987), pp. 59-71
View PDF
View articleView in ScopusGoogle Scholar
[29]
L. Lamport
What good is temporal logic?
R. Mason (Ed.), Information Processing 83: Proc. 9th IFIP World Computer Cong., Elsevier, Amsterdam (1983), pp. 657-668
View in ScopusGoogle Scholar
[30]
N. Leveson, J. Stolzy
Analyzing safety and fault tolerance using timed Petri nets
Proc. Internat. Joint Conf. on Theory and Practice of Software Development, Vol. 186, Springer, Berlin (1985), pp. 339-355
Lecture Notes in Computer Science
CrossrefView in ScopusGoogle Scholar
[31]
H. Lewis
Finite-state analysis of asynchronous circuits with bounded temporal uncertainty
Tech. Report TR-15-89, Harvard University (1989)
Google Scholar
[32]
N. Lynch, H. Attiya
Using mappings to prove timing properties
Proc. 9th ACM Symp. on Principles of Distributed Computing (1990), pp. 265-280
View in ScopusGoogle Scholar
[33]
Z. Manna, A. Pnueli
The temporal framework for concurrent programs
R. Boyer, J. Moore (Eds.), The Correctness Problem in Computer Science, Academic Press, New York (1981), pp. 215-274
Google Scholar
[34]
R. McNaughton
Testing and generating infinite sequences by a finite automaton
Inform. and Control, 9 (1966), pp. 521-530
View PDF
View articleView in ScopusGoogle Scholar
[35]
X. Nicollin, J. Sifakis, S. Yovine
From ATP to timed graphs and hybrid systems
Proc. REX workshop “Real-time: Theory in Practice”, Vol. 600, Springer, Berlin (1991), pp. 549-572
Lecture Notes in Computer Science
Google Scholar
[36]
J. Ostroff
Temporal Logic of Real-Time Systems
Research Studies Press (1990)
Google Scholar
[37]
A. Pnueli
The temporal logic of programs
Proc. 18th IEEE Symp. on Foundations of Computer Science (1977), pp. 46-77
CrossrefView in ScopusGoogle Scholar
[38]
A. Pnueli
Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends
Current Trends in Concurrency, Vol. 224, Springer, Berlin (1986), pp. 510-584
Lecture Notes in Computer Science
Google Scholar
[39]
C. Ramchandani
Analysis of asynchronous concurrent systems by Petri nets
Tech. Report MACTR-120, Massachusetts Institute of Technology (1974)
Google Scholar
[40]
H. Rogers
Theory of Recursive Functions and Effective Computability
McGraw-Hill, New York (1967)
Google Scholar
[41]
S. Safra
On the complexity of ω-automata
Proc. 29th IEEE Symp. on Foundations of Computer Science (1988), pp. 319-327
View in ScopusGoogle Scholar
[42]
A.P. Sistla, M. Vardi, P. Wolper
The complementation problem for Büchi automata with applications to temporal logic
Theoret. Comput. Sci., 49 (1987), pp. 217-237
Google Scholar
[43]
W. Thomas
Automata on infinite objects
J. van Leeuwen (Ed.), Handbook of Theoretical Computer Science, Vol. B, Elsevier, Amsterdam (1990), pp. 133-191
View PDF
View articleView in ScopusGoogle Scholar
[44]
M. Vardi
Verification of concurrent programs–the automata-theoretic framework
Proc. 2nd IEEE Symp. on Logic in Computer Science (1987), pp. 167-176
View in ScopusGoogle Scholar
[45]
M. Vardi, P. Wolper
An automata-theoretic approach to automatic program verification
Proc. 1st IEEE Symp. on Logic in Computer Science (1986), pp. 332-344
View in ScopusGoogle Scholar
[46]
P. Wolper
Temporal logic can be more expressive
Inform. and Control, 56 (1983), pp. 72-99
View PDF
View articleView in ScopusGoogle Scholar
[47]
H. Wong-Toi, G. Hoffmann
The control of dense real-time discrete event systems
Proc. 30th IEEE Conf. on Decision and Control (1991), pp. 1527-1528
View in ScopusGoogle Scholar
[48]
P. Wolper, M. Vardi, A.P. Sistla
Reasoning about infinite computation paths
Proc. 24th IEEE Symp. on Foundations of Computer Science (1983), pp. 185-194
View at publisherCrossrefView in ScopusGoogle Scholar