A theory of timed automata

Theoretical Computer Science - Tập 126 Số 2 - Trang 183-235 - 1994
Rajeev Alur1, David L. Dill1
1Stanford University, Stanford, CA

Tóm tắt

Từ khóa


Tài liệu tham khảo

Alur, 1990, Model-checking for real-time systems, Proc. 5th IEEE Symp. on Logic in Computer Science, 414, 10.1109/LICS.1990.113766

Alur, 1991, Model-checking for probabilistic real-time systems, Vol. 510, 115

Alur, 1991, Verifying automata specifications of probabilistic real-time systems, Vol. 600, 28

Alur, 1991, The benefits of relaxing punctuality, Proc. 10th ACM Symp. on Principles of Distributed Computing, 139

Alur, 1989, A really temporal logic, Proc. 30th IEEE Symp. on Foundations of Computer Science, 164, 10.1109/SFCS.1989.63473

Bernstein, 1981, Proving real-time properties of programs with temporal logic, Proc. 8th ACM Symp. on Operating System Principles, 164

Büchi, 1962, On a decision method in restricted second-order arithmetic, 1

Burch, 1992, Symbolic model checking: 1020 states and beyond, Inform. and Comput., 98, 142, 10.1016/0890-5401(92)90017-A

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).

Choueka, 1974, Theories of automata on ω-tapes: a simplified approach, J. Comput. System Sci., 8, 117, 10.1016/S0022-0000(74)80051-6

Clarke, 1989, A unified approach for showing language containment and equivalence between various types of ω-automata

Clarke, 1986, Automatic verification of finite-state concurrent systems using temporal-logic specifications, ACM Trans. Programming Languages and Systems, 8, 244, 10.1145/5397.5399

Courcoubetis, 1991, Minimum and maximum delay problems in real-time systems, Vol. 575, 399

Dill, 1989, Timing assumptions and verification of finite-state concurrent systems, Vol. 407, 197

Dill, 1989

Dill, 1990, Synthesizing processes and schedulers from temporal specifications, Vol. 531, 272

Emerson, 1982, Using branching-time temporal logic to synthesize synchronization skeletons, Sci. Comput. Programming, 2, 241, 10.1016/0167-6423(83)90017-5

Emerson, 1990, Quantitative temporal reasoning, Vol. 531, 136

Godefroid, 1991, A partial approach to model-checking, Proc. 6th IEEE Symp. on Logic in Computer Science, 406

Harel, 1990, Explicit-clock temporal logic, Proc. 5th IEEE Symp. on Logic in Computer Science, 402, 10.1109/LICS.1990.113765

Harel, 1983, Propositional dynamic logic of regular programs, J. Comput. System Sci., 26, 222, 10.1016/0022-0000(83)90014-4

Henzinger, 1991, Temporal proof methodologies for real-time systems, Proc. 18th ACM Symp. on Principles of Programming Languages, 353

Hoare, 1978, Communicating sequential processes, Comm. ACM, 21, 666, 10.1145/359576.359585

Hopcroft, 1979

Jahanian, 1986, Safety analysis of timing properties in real-time systems, IEEE Trans. Software Engrg., SE-12, 890, 10.1109/TSE.1986.6313045

Jahanian, 1987, A graph-theoretic approach for timing analysis and its implementation, IEEE Trans. Comput., C-36, 961, 10.1109/TC.1987.5009519

Koymans, 1990, Specifying real-time properties with metric temporal logic, J. Real-time Systems, 2, 255, 10.1007/BF01995674

Kurshan, 1987, Complementing deterministic Büchi automata in polynomial time, J. Comput. System Sci., 35, 59, 10.1016/0022-0000(87)90036-5

Lamport, 1983, What good is temporal logic?, 657

Leveson, 1985, Analyzing safety and fault tolerance using timed Petri nets, Vol. 186, 339

Lewis, 1989, Finite-state analysis of asynchronous circuits with bounded temporal uncertainty

Lynch, 1990, Using mappings to prove timing properties, Proc. 9th ACM Symp. on Principles of Distributed Computing, 265, 10.1145/93385.93428

Manna, 1981, The temporal framework for concurrent programs, 215

McNaughton, 1966, Testing and generating infinite sequences by a finite automaton, Inform. and Control, 9, 521, 10.1016/S0019-9958(66)80013-X

Nicollin, 1991, From ATP to timed graphs and hybrid systems, Vol. 600, 549

Ostroff, 1990

Pnueli, 1977, The temporal logic of programs, Proc. 18th IEEE Symp. on Foundations of Computer Science, 46

Pnueli, 1986, Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends, Vol. 224, 510

Ramchandani, 1974, Analysis of asynchronous concurrent systems by Petri nets

Rogers, 1967

Safra, 1988, On the complexity of ω-automata, Proc. 29th IEEE Symp. on Foundations of Computer Science, 319, 10.1109/SFCS.1988.21948

Sistla, 1987, The complementation problem for Büchi automata with applications to temporal logic, Theoret. Comput. Sci., 49, 217, 10.1016/0304-3975(87)90008-9

Thomas, 1990, Automata on infinite objects, 133

Vardi, 1987, Verification of concurrent programs–the automata-theoretic framework, Proc. 2nd IEEE Symp. on Logic in Computer Science, 167

Vardi, 1986, An automata-theoretic approach to automatic program verification, Proc. 1st IEEE Symp. on Logic in Computer Science, 332

Wolper, 1983, Temporal logic can be more expressive, Inform. and Control, 56, 72, 10.1016/S0019-9958(83)80051-5

Wong-Toi, 1991, The control of dense real-time discrete event systems, Proc. 30th IEEE Conf. on Decision and Control, 1527, 10.1109/CDC.1991.261658

Wolper, 1983, Reasoning about infinite computation paths, Proc. 24th IEEE Symp. on Foundations of Computer Science, 185