{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T04:21:16Z","timestamp":1775881276796,"version":"3.50.1"},"reference-count":264,"publisher":"Elsevier","isbn-type":[{"value":"9780444508133","type":"print"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1016\/b978-044450813-3\/50026-6","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T13:04:11Z","timestamp":1181567051000},"page":"1635-1790","source":"Crossref","is-referenced-by-count":365,"title":["Model Checking"],"prefix":"10.1016","author":[{"given":"Edmund M.","family":"Clarke","sequence":"first","affiliation":[]},{"given":"Bernd-Holger","family":"Schlingloff","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/B978-044450813-3\/50026-6_bb0010","series-title":"Formal System Specification: The RPC-Memory Specification Case Study","first-page":"21","article-title":"A TLA solution to the RPC-memory specification problem","author":"Abadi","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0015","series-title":"Proc. 4th Int. Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '98)","first-page":"281","article-title":"Model checking via reachability testing for timed automata","author":"Aceto","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0020","series-title":"The Design and Analysis of Computer Algorithms","author":"Aho","year":"1974"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0025","doi-asserted-by":"crossref","first-page":"1004","DOI":"10.1145\/31846.31852","article-title":"Monotone versus positive","volume":"34","author":"Ajtai","year":"1987","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0030","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","article-title":"Defining liveness","volume":"21","author":"Alpern","year":"1985","journal-title":"Information Processing Letters"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0035","article-title":"Techniques for Automatic Verification of Real-Time Systems","author":"Alur","year":"1991","journal-title":"PhD thesis, Stanford University"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0040","series-title":"Verification of Digital and Hybrid Systems","article-title":"Timed automata","author":"Alur","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0045","series-title":"Proc. 9th Int. Conf. on Computer Aided Verification (CAV '97)","first-page":"340","article-title":"Partial-order reduction in symbolic state space exploration","author":"Alur","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0050","series-title":"Proc. 5th Ann. IEEE Symp. on Logic in Computer Science (LICS '90)","first-page":"414","article-title":"Model-checking for real-time systems","author":"Alur","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0055","series-title":"Proc. 17th Int. Conf. on Automata, Languages and Programming (ICALP '90)","first-page":"322","article-title":"Automata for modelling real-time systems","author":"Alur","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0060","series-title":"Real-Time: Theory in Practice","article-title":"Logics and models of real-time: A survey","author":"Alur","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0065","series-title":"Logic at St. Petersburg. Symp. on Logical Foundations of Computer Science (LFCS '94)","article-title":"On model checking infinite-state systems","author":"Andersen","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0070","series-title":"Proc. 9th Ann. IEEE Symp. on Logic in Computer Science (LICS '94)","first-page":"144","article-title":"A compositional proof system for the modal \u00b5-calculus","author":"Andersen","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0075","article-title":"Synthesis of Reactive Programs","author":"Anuchitanukul","year":"1995","journal-title":"PhD thesis, Stanford"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0080","series-title":"IEEE Real-Time Technology and Applications Symp. (RTAS'96)","article-title":"Mechanical verification of timed automata: A case study","author":"Archer","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0085","series-title":"Proc. 8th Workshop on Computer Aided Verification (CAV '96)","first-page":"269","article-title":"Verifying continuous Markov chains","author":"Aziz","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0090","series-title":"Proc. 7th Workshop on Computer Aided Verification (CAV '95)","first-page":"155","article-title":"It usually works \u2013 the temporal logic of stochastic systems","author":"Aziz","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50026-6_rf0095","series-title":"Proc. Int. Conf. on Computer Aided Design (ICCAD '93)","first-page":"188","article-title":"Algebraic decision diagrams and their applications","author":"Bahar","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0100","series-title":"Proc. Int. Conf. on Automata, Languages and Programming (ICALP '97)","first-page":"430","article-title":"Symbolic model checking for probabilistic processes","author":"Baier","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0105","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/BF01257083","article-title":"The temporal logic of branching time","volume":"20","author":"Ben-Ari","year":"1983","journal-title":"Acta Informatica"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0110","series-title":"Proc. 4th Int. Conf. on Computer Aided Verification (CAV '92)","article-title":"Property preserving simulations","author":"Bensalem","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0115","article-title":"Model checking algorithms for the \u00b5-calculus","author":"Berezin","year":"1996","journal-title":"Technical Report CMU-CS-96-180, CMU"},{"issue":"8","key":"10.1016\/B978-044450813-3\/50026-6_bb0120","doi-asserted-by":"crossref","first-page":"1059","DOI":"10.1109\/43.85742","article-title":"Circuit width, register allocation and ordered binary decision diagrams","volume":"10","author":"Bermann","year":"1991","journal-title":"IEEE Trans. on Computer-Aided Design"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0125","series-title":"Proc. 7th Workshop on Computer Aided Verification (CAV '95)","first-page":"4","article-title":"Global rebuilding of BDDs \u2013 avoiding the memory requirement maxima","author":"Bern","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0130","series-title":"Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '96)","first-page":"107","article-title":"Efficient local model checking for fragments of the modal \u00b5-calculus","author":"Bhat","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0135","article-title":"Effiziente Modellpr\u00fcfung des \u00b5-Kalk\u00fcls mit bin\u00e4ren Entscheidungsdiagrammen","author":"Biere","year":"1997","journal-title":"PhD thesis, University of Karlsruhe, Germany"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0140","series-title":"Proc. 36th ACM\/IEEE Design Automation Conference (DAC '99)","article-title":"Symbolic model checking using SAT procedures instead of BDDs","author":"Biere","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0145","series-title":"Proc. Tools and Algorithms for the Analysis and Construction of Systems (TACAS'99)","article-title":"Symbolic model checking without BDDs","author":"Biere","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0150","article-title":"STeP: The Stanford theorem prover \u2013 user's manual","author":"Bj\u00f8rner","year":"1995","journal-title":"Technical Report STAN-CS-TR-95-1562, Department of Computer Science, Stanford University"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0155","series-title":"Proc. 8th Workshop Computer Aided Verification (CAV '96)","article-title":"STeP: Deductive-algorithmic verification of reactive and real-time systems","author":"Bj\u00f8rner","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0160","series-title":"Modal Logic","author":"Blackburn","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0165","series-title":"Proc. 8th Workshop on Computer Aided Verification (CAV '96)","first-page":"1","article-title":"Symbolic verification of communication protocols with infinite state spaces using qdds","author":"Boigelot","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0170","series-title":"Proc. 9th Workshop on Computer Aided Verification (CAV '97)","article-title":"The industrial success of verification tools based on stlmarck's method","author":"Bor\u00e4lv","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0175","series-title":"Proc. 27th ACM\/IEEE Design Automation Conference (DAC '90)","first-page":"40","article-title":"Efficient implementation of a BDD package","author":"Brace","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0180","series-title":"Proc. 3rd Workshop on Computer Aided Verification (CAV '91)","article-title":"Local model checking for infinite state spaces","author":"Bradfield","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0185","series-title":"IFIP WG 10. 2 Int. Working Conf. from HDL Descriptions to Guaranteed Correct Circuit Designs","article-title":"SML: A high level language for the design and verification of finite state machines","author":"Browne","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0190","series-title":"Proc. 1985 Int IEEE Conf. on Computer Design","article-title":"Checking the correctness of sequential circuits","author":"Browne","year":"1985"},{"key":"10.1016\/B978-044450813-3\/50026-6_rf0195","series-title":"Formal Aspects of VLSI Design","article-title":"Automatic circuit verification using temporal logic: Two new examples","author":"Browne","year":"1986"},{"issue":"1\u20132","key":"10.1016\/B978-044450813-3\/50026-6_bb0200","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","article-title":"Characterizing finite Kripke structures in propositional temporal logic","volume":"59","author":"Browne","year":"1988","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50026-6_bb0205","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1016\/0890-5401(89)90026-6","article-title":"Reasoning about networks with many identical finite-state processes","volume":"81","author":"Browne","year":"1989","journal-title":"Information and Computation"},{"issue":"12","key":"10.1016\/B978-044450813-3\/50026-6_bb0210","doi-asserted-by":"crossref","first-page":"1035","DOI":"10.1109\/TC.1986.1676711","article-title":"Automatic verification of sequential circuits using temporal logic","volume":"C-35","author":"Browne","year":"1986","journal-title":"IEEE Trans. on Computers"},{"issue":"8","key":"10.1016\/B978-044450813-3\/50026-6_bb0215","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-based algorithms for Boolean function manipulation","volume":"C-35","author":"Bryant","year":"1986","journal-title":"IEEE Trans. on Computers"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50026-6_bb0220","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1109\/12.73590","article-title":"On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication","volume":"40","author":"Bryant","year":"1991","journal-title":"IEEE Trans. on Computers"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50026-6_bb0225","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","article-title":"Symbolic Boolean manipulation with ordered binary decision diagrams","volume":"24","author":"Bryant","year":"1992","journal-title":"ACM Computing Surveys"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0230","series-title":"Proc. Int. Congr. Logic, Method and Philosophy of Science 1960","first-page":"1","article-title":"On a decision method in restricted second order arithmetic","author":"B\u00fcchi","year":"1962"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50026-6_bb0235","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1109\/43.275352","article-title":"Symbolic model checking for sequential circuit verification","volume":"13","author":"Burch","year":"1994","journal-title":"IEEE Trans. on Computer Aided Design of Integrated Circuits"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0240","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1098\/rsta.1992.0028","article-title":"Automatic verification of sequential circuit designs","volume":"339","author":"Burch","year":"1992","journal-title":"Phil. Trans. R. Soc. Lond. A"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0245","series-title":"Proc. 28th ACM\/IEEE Design Automation Conference (DAC '91)","article-title":"Representing circuits more efficiently in symbolic model checking","author":"Burch","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0250","series-title":"Proc. Int. Conf. on Very Large Scale Integration (VLSI '91)","article-title":"Symbolic model checking with partitioned transition relations","author":"Burch","year":"1991"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50026-6_bb0255","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","article-title":"Symbolic model checking: 1020 states and beyond","volume":"98","author":"Burch","year":"1992","journal-title":"Information and Computation"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0260","series-title":"Proc. 27th ACM\/IEEE Design Automation Conference (DAC '90)","article-title":"Sequential circuit verification using symbolic model checking","author":"Burch","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0265","series-title":"Handbook of Philosophical Logic","first-page":"89","article-title":"Basic tense logic","author":"Burgess","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0270","article-title":"More infinite results","volume":"6","author":"Burkart","year":"1997","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0275","article-title":"A logic of authentication","author":"Burrows","year":"1989","journal-title":"Technical Report 39, DEC Systems Research Center"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0280","series-title":"Proc. IFIP Congress","first-page":"308","article-title":"Program proving as hand simulation with a little induction","author":"Burstall","year":"1974"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0285","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1016\/0022-0000(80)90032-X","article-title":"Computable queries for relational databases","volume":"21","author":"Chandra","year":"1980","journal-title":"J. of Computer and System Sciences"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0290","series-title":"Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency","first-page":"428","article-title":"Expressibility results for linear time and branching time logics","author":"Clarke","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50026-6_rf0295","series-title":"Proc. 15th Coll. on Trees in Algebra and Programming","article-title":"A unified approach for showing language containment and equivalence between various types of ?-automata","author":"Clarke","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0300","series-title":"Proc. Workshop on Logic of Programs","article-title":"Synthesis of synchronization skeletons for branching time temporal logic","author":"Clarke","year":"1981"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50026-6_bb0305","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic verification of finite-state concurrent systems using temporal logic specifications","volume":"8","author":"Clarke","year":"1986","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0310","series-title":"Proc. 5th Workshop on Computer Aided Verification (CAV '93)","article-title":"Exploiting symmetry in temporal logic model checking","author":"Clarke","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0315","series-title":"Proc. 1st Int. Conf. on Information, Communications and Signal Processing (ICICS '97)","article-title":"Hybrid spectral transform diagrams","author":"Clarke","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0320","series-title":"Proc. Int. Workshop on Logic Synthesis (IWLS '93)","article-title":"Multi-terminal binary decision diagrams: An efficient data structure for matrix representation","author":"Clarke","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0325","series-title":"Proc. IEEE Int. Conf. on Computer Aided Design (ICCAD '95)","first-page":"54","article-title":"Hybrid decision diagrams \u2013 overcoming the limitations of MTBDDs and BMDs","author":"Clarke","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0330","series-title":"Representations of Discrete Functions","first-page":"93","article-title":"Multi-terminal binary decision diagrams and hybrid decision diagrams","author":"Clarke","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0335","series-title":"Proc. 6th Ann. ACM Symp. on Principles of Distributed Computing","first-page":"294","article-title":"Avoiding the state explosion problem in temporal model checking algorithms","author":"Clarke","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0340","article-title":"Research on automatic verification of finite-state concurrent systems","author":"Clarke","year":"1987","journal-title":"Technical Report CMU-CS-87-105, Carnegie Mellon University"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0345","series-title":"Proc. 5th Ann. ACM Symp. on Principles of Distributed Computing","first-page":"240","article-title":"Reasoning about networks with many identical finite-state processes","author":"Clarke","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0350","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1023\/A:1008615614281","article-title":"Another look at LTL model checking","volume":"10","author":"Clarke","year":"1997","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0355","series-title":"Proc. 11th Int. Symp. on Computer Hardware Description Languages and their Applications","article-title":"Verification of the Futurebus+ cache coherence protocol","author":"Clarke","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0360","series-title":"Proc. 6th Int. Conf. on Concurrency Theory (CONCUR '95)","article-title":"Parametrized networks","author":"Clarke","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0365","series-title":"Deductive Program Design","first-page":"305","article-title":"Model checking","author":"Clarke","year":"1993"},{"issue":"5","key":"10.1016\/B978-044450813-3\/50026-6_bb0370","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","article-title":"Model checking and abstraction","volume":"16","author":"Clarke","year":"1994","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/B978-044450813-3\/50026-6_rf0375","series-title":"A Decade of Concurrency \u2013 Reflections and Perspectives","first-page":"124","article-title":"Verification tools for finite-state concurrent systems","author":"Clarke","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50026-6_rf0380","series-title":"REX School\/Symposium","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0380","article-title":"Efficient generation of counterexamples and witnesses in symbolic model checking","author":"Clarke","year":"1994","journal-title":"Technical Report CMU-CS-94-204, Carnegie Mellon University, Pittsburgh"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0385","doi-asserted-by":"crossref","DOI":"10.1007\/s100090050035","article-title":"State space reductions using partial order techniques","author":"Clarke","year":"1999","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"10.1016\/B978-044450813-3\/50026-6_rf0395","series-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0395","series-title":"Equivalence checking using abstract BDDs","author":"Clarke","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0400","series-title":"Proc. 30th ACM\/IEEE Design Automation Conference (DAC '93)","article-title":"Word level model checking \u2013 a new approach for verifying arithmetic circuits","author":"Clarke","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0405","series-title":"Shared Memory Multiprocessing","first-page":"53","article-title":"Symbolic computation algorithms on shared memory multiprocessors","author":"Clarke","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0410","series-title":"Proc. 4th Ann. IEEE Symp. on Logic in Computer Science (LICS '89)","article-title":"Compositional model checking","author":"Clarke","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0415","first-page":"1283","article-title":"A language for compositional specification and verification of finite state hardware controllers","volume":"79","author":"Clarke","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0420","series-title":"Proc. 30th ACM\/IEEE Design Automation Conference (DAC '93)","first-page":"54","article-title":"Spectral transforms for large Boolean functions with applications to technology mapping","author":"Clarke","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0425","series-title":"Proc. Workshop on Logics of Programs","first-page":"101","article-title":"Automatic verification of asynchronous circuits","author":"Clarke","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0430","series-title":"12th Int. Conf. on Automated Deduction (CADE '94)","first-page":"758","article-title":"Combining symbolic computation and theorem proving: some problems of Ramanujan","author":"Clarke","year":"1994"},{"issue":"8","key":"10.1016\/B978-044450813-3\/50026-6_bb0435","doi-asserted-by":"crossref","first-page":"725","DOI":"10.1007\/BF00264284","article-title":"Tableau-based model checking in the propositional \u00b5-calculus","volume":"27","author":"Cleaveland","year":"1990","journal-title":"Acta Informatica"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50026-6_bb0440","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/BF01383878","article-title":"A linear-time model-checking algorithm for the alternation-free modal \u00b5-calculus","volume":"2","author":"Cleaveland","year":"1993","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0445","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/BF00121128","article-title":"Memory efficient algorithms for the verification of temporal properties","volume":"1","author":"Courcoubetis","year":"1992","journal-title":"Formal Methods in System Design"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50026-6_bb0450","doi-asserted-by":"crossref","first-page":"857","DOI":"10.1145\/210332.210339","article-title":"The complexity of probabilistic verification","volume":"42","author":"Courcoubetis","year":"1995","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0455","series-title":"Proc. 4th Ann. ACM Symp. on Principles of Programming Languages (POPL '77)","article-title":"Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints","author":"Cousot","year":"1977"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0460","series-title":"Proc. 6th Ann. ACM Symp. on Principles of Programming Languages (POPL '79)","article-title":"Systematic design of program analysis frameworks","author":"Cousot","year":"1979"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0465","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0304-3975(94)90269-0","article-title":"CTL* and ECTL* as fragments of the modal \u00b5-calculus","volume":"126","author":"Dam","year":"1994","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0470","series-title":"Proc. 6th Int. Conf. on Concurrency Theory (CONCUR '95)","first-page":"12","article-title":"Compositional proof systems for model checking infinite state processes","author":"Dam","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0475","article-title":"Abstract interpretation and partition refinement for model checking","author":"Dams","year":"1995","journal-title":"PhD thesis, Technical University Eindhoven"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0480","series-title":"Programming Concepts, Methods and Calculi (PROCOMET '94)","first-page":"561","article-title":"Abstract interpretation of reactive systems: Abstractions preserving ?CTL*, ?CTL* and CTL*","author":"Dams","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0485","series-title":"Cambridge Mathematical Textbooks","article-title":"Introduction to Lattices and Order","author":"Davey","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0490","series-title":"Proc. Computer Science Logic (CSL '95)","first-page":"161","article-title":"First order logic, fixed point logic and linear order","author":"Dawar","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50026-6_rf0500","series-title":"Compositionality: The Significant Difference","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0500","series-title":"Proc. Int. Workshop on Automatic Verification Methods for Finite State Systems","first-page":"197","article-title":"Timing assumptions and verification of finite-state concurrent systems","author":"Dill","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0505","article-title":"Automatic verification of asynchronous circuits using temporal logic","volume":"133","author":"Dill","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0510","series-title":"Proc. 7th Workshop on Computer Aided Verification (CAV '95)","first-page":"45","article-title":"Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving","author":"Dingel","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0515","series-title":"Proc. KI-98: Advances in Artificial Intelligence","first-page":"81","article-title":"OBDDs in heuristic search","author":"Edelkamp","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0520","doi-asserted-by":"crossref","first-page":"129","DOI":"10.4064\/fm-49-2-129-141","article-title":"An application of games to the completeness problem for formalized theories","volume":"49","author":"Ehrenfeucht","year":"1961","journal-title":"Fund. Math."},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0525","series-title":"Proc. Int. Conf. on Logics of Programs","first-page":"79","article-title":"Automata, tableaux, and temporal logic","author":"Emerson","year":"1985"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0530","first-page":"997","article-title":"Temporal and modal logic","volume":"Vol. B","author":"Emerson","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0535","series-title":"Proc. 17th Int. Coll. on Automata, Languages and Programming (ICALP '80)","first-page":"169","article-title":"Characterizing correctness properties of parallel programs using fixpoints","author":"Emerson","year":"1980"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0540","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","article-title":"Using branching time logic to synthesize synchronization skeletons","volume":"2","author":"Emerson","year":"1982","journal-title":"Science of Computer Programming"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50026-6_bb0545","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","article-title":"Decision procedures and expressiveness in the temporal logic of branching time","volume":"30","author":"Emerson","year":"1985","journal-title":"Journal of Computer and System Sciences"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0550","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","article-title":"\u201csometimes\u201d and \u201cnot never\u201d revisited: on branching time vs. linear time","volume":"33","author":"Emerson","year":"1986","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0555","series-title":"Proc. 5th Workshop on Computer Aided Verification (CAV '93)","article-title":"On model-checking for fragments of \u00b5-calculus","author":"Emerson","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0560","series-title":"Proc. 12th Symp. on Principles of Programming Languages (POPL '85)","article-title":"Modalities for model checking: Branching time strikes back","author":"Emerson","year":"1985"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0565","series-title":"Proc. 1st Symp. on Logic in Computer Science (LICS '86)","article-title":"Efficient model checking in fragments of the propositional \u00b5-calculus","author":"Emerson","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0570","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/S0019-9958(84)80047-9","article-title":"Deciding full branching time logic","volume":"61","author":"Emerson","year":"1984","journal-title":"Information and Control"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0575","series-title":"Proc. 5th Workshop on Computer Aided Verification (CAV '93)","article-title":"Symmetry and model checking","author":"Emerson","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0580","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/BF02242704","article-title":"Generating BDDs for symbolic model checking","volume":"6","author":"Enders","year":"1993","journal-title":"Distributed Computing"},{"issue":"2\u20133","key":"10.1016\/B978-044450813-3\/50026-6_bb0585","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/0167-6423(94)00019-0","article-title":"Model checking using net unfoldings","volume":"23","author":"Esparza","year":"1994","journal-title":"Science of Computer Programming"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0590","series-title":"Proc. European Design Automation Conference (EuroDAC '93)","first-page":"130","article-title":"Dynamic variable reordering for BDD minimization","author":"Felt","year":"1993"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50026-6_bb0595","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","article-title":"Propositional dynamic logic of regular programs","volume":"18","author":"Fischer","year":"1979","journal-title":"Journal of Computer and System Sciences"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0600","series-title":"Proof methods for modal and intuitionistic logics","author":"Fitting","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50026-6_rf0610","series-title":"Sur quelques classifications des syst\u00e8mes de relations","author":"Fra\u00efss\u00e9","year":"1954"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0610","series-title":"Text and Monographs in Computer Science","article-title":"Fairness","author":"Francez","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0615","series-title":"Proc. Int. Conf. on Computer Aided Design (ICCAD'93)","article-title":"Interleaving based variable ordering methods for ordered binary decision diagrams","author":"Fuji","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0620","series-title":"Temporal Logic in Specification","first-page":"431","article-title":"The declarative past and imperative future: Executable temporal logic for interactive systems","author":"Gabbay","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0625","series-title":"Temporal Logic: Mathematical Foundations and Computational Aspects","author":"Gabbay","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0630","series-title":"Proc. 7th ACM Symp. on Principles of Programming Languages (POPL '80)","first-page":"163","article-title":"On the temporal analysis of fairness","author":"Gabbay","year":"1980"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0635","doi-asserted-by":"crossref","first-page":"675","DOI":"10.1145\/146637.146681","article-title":"Reasoning about systems with many processes","volume":"39","author":"German","year":"1992","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0640","series-title":"Proc. 3rd Israel Symp. on the Theory of Computing and Systems (ISTCS '95)","first-page":"130","article-title":"A partial order approach to branching time logic model checking","author":"Gerth","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0645","series-title":"Proc. 2nd Workshop on Computer Aided Verification (CAV '90)","first-page":"176","article-title":"Using partial orders to improve automatic verification methods","author":"Godefroid","year":"1990"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50026-6_bb0650","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01384077","article-title":"State-space caching revisited","volume":"7","author":"Godefroid","year":"1995","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0655","series-title":"Proc. 11th Ann. IEEE Symp. on Logic in Computer Science (LICS '96)","article-title":"Symbolic protocol verification with queue BDDs","author":"Godefroid","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0660","series-title":"Proc. 5th Workshop on Computer Aided Verification (CAV '93)","first-page":"438","article-title":"Refining dependencies improves partial-order verification methods","author":"Godefroid","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0665","series-title":"Proc. 6th Ann. IEEE Symp. on Logic in Computer Science (LICS '91)","first-page":"406","article-title":"A partial approach to model checking","author":"Godefroid","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0670","series-title":"Proc. 2nd Workshop on Computer Aided Verification (CAV '90)","article-title":"Compositional minimization of finite state processes","author":"Graf","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0675","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","article-title":"Model checking and modular verification","volume":"16","author":"Grumberg","year":"1994","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0680","first-page":"633","article-title":"Semantic domains","volume":"Vol. B","author":"Gunter","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0685","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1016\/0168-0072(86)90055-2","article-title":"Fixed-point extensions of first-order logic","volume":"32","author":"Gurevich","year":"1986","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0690","series-title":"Proc. Int. Workshop on Verification of Infinite State Systems (INFINITY '96)","first-page":"149","article-title":"A modal \u00b5-calculus and a proof system for value passing processes","author":"Gurov","year":"1996"},{"issue":"12","key":"10.1016\/B978-044450813-3\/50026-6_bb0695","doi-asserted-by":"crossref","first-page":"1479","DOI":"10.1109\/43.552081","article-title":"Markovian analysis of large finite state machines","volume":"15","author":"Hachtel","year":"1996","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0700","series-title":"Proc. 10th IEEE Real-Time Systems Symp.","first-page":"102","article-title":"A framework for reasoning about time and reliability","author":"Hansson","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0705","series-title":"Handbook of Philosophical Logic","first-page":"488","article-title":"Dynamic logic","author":"Harel","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50026-6_rf0715","series-title":"Logics and Models of Concurrent Systems","first-page":"477","article-title":"On the development of reactive systems","author":"Harel","year":"1985"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50026-6_bb0715","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1002\/j.1538-7305.1990.tb00102.x","article-title":"Software for analytical development of communications protocols","volume":"69","author":"Har'El","year":"1990","journal-title":"AT&T Tech. J."},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0720","article-title":"Timed transition systems","author":"Henzinger","year":"1992","journal-title":"Technical Report TR 92-1263, Dept. of CS, Cornell Univ."},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0725","series-title":"Design and Validation of Computer Protocols","author":"Holzmann","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0730","series-title":"Proc. 15th Int. Conf. on Protocol Specification, Testing and Verification","first-page":"301","article-title":"An analysis of bitstate hashing","author":"Holzmann","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0735","series-title":"Introduction to Automata Theory, Languages, and Computation","author":"Hopcroft","year":"1979"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0740","series-title":"An Introduction to Modal Logic","author":"Hughes","year":"1977"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0745","series-title":"IEEE Standard for the Futurebus+ Logical Protocol Specification","author":"IEEE","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0750","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1016\/S0019-9958(86)80029-8","article-title":"Relational queries computable in polynomial time","volume":"68","author":"Immerman","year":"1986","journal-title":"Information and Control"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0755","series-title":"Proc. 11th Int. Symp. on Computer Hardware Description Languages and their Applications","article-title":"Better verification through symmetry","author":"Ip","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0760","series-title":"Proc. 7th Int. Conf. on Concurrency Theory (CONCUR '96)","article-title":"On the expressive completeness of the propositional \u00b5-calculus with respect to monadic second order logic","author":"Janin","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0765","series-title":"Modular specification and verification of reactive systems","author":"Josko","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0770","article-title":"Tense Logic and the Theory of Linear Order","author":"Kamp","year":"1968","journal-title":"PhD thesis, Univ. of Calif., Los Angeles"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50026-6_bb0775","doi-asserted-by":"crossref","first-page":"808","DOI":"10.1145\/6490.6496","article-title":"Polynomial-time algorithm for the orbit problem","volume":"33","author":"Kannan","year":"1986","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0780","series-title":"Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency","article-title":"An efficient verification method for parallel and distributed programs","author":"Katz","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0785","series-title":"Proc. 10th Ann. IEEE Symp. on Logic in Computer Science (LICS '95)","first-page":"2","article-title":"A complete axiomatization of qptl","author":"Kesten","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0790","series-title":"Proc. 32nd Int. Design Automation Conference (DAC '95)","article-title":"Residue BDD and its application to the verification of arithmetic circuits","author":"Kimura","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0795","series-title":"USENIX 2nd Workshop on Electronic Commerce","article-title":"Fast, automatic checking of security protocols","author":"Kindred","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0800","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","article-title":"Results on the propositional \u00b5-calculus","volume":"27","author":"Kozen","year":"1983","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0805","series-title":"Proc. Int. Symp. Logic of Programs","article-title":"A decision procedure for the propositional \u00b5-calculus","author":"Kozen","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0810","first-page":"791","article-title":"Logics of programs","volume":"Vol. B","author":"Kozen","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0815","first-page":"83","article-title":"Semantical considerations on modal logic","volume":"16","author":"Kripke","year":"1963","journal-title":"Acta Philosophica Fennica"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0820","doi-asserted-by":"crossref","first-page":"690","DOI":"10.2307\/2024634","article-title":"Outline of a theory of truth","volume":"72","author":"Kripke","year":"1975","journal-title":"Journal of Philosophy"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0825","series-title":"Proc. IFIP Work. Conf. Formal Desription of Programming Concepts","first-page":"441","article-title":"A uniform logical basis for the description, specification and verification of programs","author":"Kr\u00f6ger","year":"1978"},{"key":"10.1016\/B978-044450813-3\/50026-6_rf0835","series-title":"EATCS monographs on TCS","article-title":"Temporal logic of Programs","author":"Kr\u00f6ger","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0835","series-title":"Proc. 8th Workshop on Computer Aided Verification (CAV '96)","first-page":"372","article-title":"Verification of fair transition systems","author":"Kupferman","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0840","series-title":"Proc. REX Workshop on Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness","article-title":"Analysis of discrete event coordination","author":"Kurshan","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0845","series-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"Kurshan","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0850","series-title":"Proc. Int. Conf. on Computer Aided Design (ICCAD '97)","article-title":"Verifying hardware in its software context","author":"Kurshan","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0855","series-title":"Proc. 8th Ann. ACM Symp. on Principles of Distributed Computing","article-title":"A structural induction theorem for processes","author":"Kurshan","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0860","series-title":"Proc. 7th Ann. ACM Symp. on Principles of Programming Languages (POPL '80)","first-page":"174","article-title":"\u201csometimes\u201d is sometimes \u201cnot never\u201d","author":"Lamport","year":"1980"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0865","series-title":"Proc. IFIP","first-page":"657","article-title":"What good is temporal logic?","author":"Lamport","year":"1983"},{"issue":"1\/2","key":"10.1016\/B978-044450813-3\/50026-6_bb0870","article-title":"Uppaal in a nutshell","volume":"1","author":"Larsen","year":"1997","journal-title":"Software Tools for Technology Transfer"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0875","series-title":"Proc. Int. Conf. on Automata, Languages, and Programming (ICALP '81)","article-title":"Impartiality, justice, and fairness: The ethics of concurrent termination","author":"Lehmann","year":"1981"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0880","doi-asserted-by":"crossref","first-page":"522","DOI":"10.1093\/mind\/XXI.84.522","article-title":"Implication and the algebra of logic","volume":"21","author":"Lewis","year":"1912","journal-title":"Mind"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0885","series-title":"Proc. 12th Ann. ACM Symp. on Principles of Programming Languages (POPL '85)","article-title":"Checking that finite state concurrent programs satisfy their linear specification","author":"Lichtenstein","year":"1985"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0890","series-title":"Proc. Int. Conf. Logics of Programs","first-page":"196","article-title":"The glory of the past","author":"Lichtenstein","year":"1985"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50026-6_bb0895","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/BF01384313","article-title":"Property preserving abstractions for the verification of concurrent systems","volume":"6","author":"Loiseaux","year":"1995","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0900","article-title":"Model Checking, Abstraction and Compositional Verification","author":"Long","year":"1993","journal-title":"PhD thesis, CMU School of Computer Science"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0905","series-title":"Proc. 6th Workshop on Computer Aided Verification (CAV '94)","first-page":"338","article-title":"An improved algorithm for the evaluation of fixpoint expressions","author":"Long","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0910","series-title":"Proc. 4th Workshop on Computer Aided Verification (CAV '92)","article-title":"Tableau recycling","author":"Mader","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0915","series-title":"Verification of concurrent programs: The temporal framework","author":"Manna","year":"1981"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0920","series-title":"Proc. Workshop on Logics of Programs","first-page":"200","article-title":"Verification of concurrent programs: Temporal proof principles","author":"Manna","year":"1982"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0925","series-title":"The Correctness Problem in Computer Science","first-page":"215","article-title":"Verification of concurrent programs: The temporal framework","author":"Manna","year":"1982"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0930","series-title":"Proc. 6th Ann. ACM Symp. on Principles of Distributed Computing","article-title":"A hierarchy of temporal properties","author":"Manna","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0935","series-title":"Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency","first-page":"201","article-title":"The anchored version of the temporal framework","author":"Manna","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50026-6_rf0945","series-title":"The Temporal Logic of Reactive and Concurrent Systems \u2013 Specification","author":"Manna","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0945","series-title":"Temporal Verifications of Reactive Systems \u2013 Safety","author":"Manna","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0950","article-title":"Gormel \u2013 grammar oriented model checker","author":"Marelly","year":"1991","journal-title":"Technical Report 697, The Technion"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0955","series-title":"Proc. 4th Workshop on Computer Aided Verification","first-page":"164","article-title":"Using unfoldings to avoid the state space explosion problem in the verification of asynchronous circuits","author":"McMillan","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0960","series-title":"Symbolic Model Checking","author":"McMillan","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0965","series-title":"Proc. Int. Symp. on Shared Memory Multiprocessing","first-page":"111","article-title":"Formal verification of the Encore Gigamax cache consistency protocol","author":"McMillan","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0970","series-title":"Proc. 2nd Int. Conf. on the Practical Applications of Prolog","article-title":"The NRL protocol analyzer: An overview","author":"Meadows","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0975","article-title":"Abstraction as a proof rule","author":"Merz","year":"1997","journal-title":"Technical report, Universit\u00e4t M\u00fcnchen"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0980","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","article-title":"A Calculus of Communicating Systems","author":"Milner","year":"1980"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0985","series-title":"Proc. Concur 99","article-title":"Partial order reduction for model checking of timed automata","author":"Minea","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0990","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0304-3975(85)90223-3","article-title":"Hierarchical verification of asynchonous circuits using temporal logic","volume":"38","author":"Mishra","year":"1985","journal-title":"Theoretical computer science"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb0995","series-title":"Proc. 1997 IEEE Symp. on Security and Privacy","article-title":"Automated analysis of cryptographic protocols using Murf","author":"Mitchell","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1000","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/BF00881842","article-title":"Introduction to OBDD algorithm for the ATP community","volume":"12","author":"Moore","year":"1994","journal-title":"Journal of automated reasoning"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1005","series-title":"Proc. 3rd Ann. IEEE Symp. on Logic in Computer Science (LICS '88)","first-page":"402","article-title":"Fixed points vs. infinite generation","author":"Niwinsky","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1010","series-title":"Digital Circuits","author":"Nowicki","year":"1990"},{"issue":"6","key":"10.1016\/B978-044450813-3\/50026-6_bb1015","doi-asserted-by":"crossref","DOI":"10.1137\/0216062","article-title":"Three efficient algorithms based on partition refinement","volume":"16","author":"Paige","year":"1987","journal-title":"SIAM journal on computing"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1020","article-title":"Finiteness is mu-ineffable","author":"Park","year":"1974","journal-title":"Theory of Computation Report 3, University of Warwick"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1025","series-title":"Theoretical Computer Science: 5th GI-Conference, Karlsruhe","first-page":"167","article-title":"Concurrency and automata on infinite sequences","author":"Park","year":"1981"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1030","series-title":"Proc. 5th Workshop Computer Aided Verification (CAV '93)","article-title":"All from one, one for all: on model checking using representatives","author":"Peled","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1035","doi-asserted-by":"crossref","DOI":"10.1016\/S0020-0190(97)00133-6","article-title":"Stutter-invariant temporal properties are expressible without the nexttime operator","author":"Peled","year":"1997","journal-title":"Information Processing Letters"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1040","series-title":"Proc. 18th Ann. IEEE Symp. on Found. of Comp. Science (FOCS '77)","first-page":"46","article-title":"The temporal logic of programs","author":"Pnueli","year":"1977"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1045","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","article-title":"The temporal semantics of concurrent programs","volume":"13","author":"Pnueli","year":"1981","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1050","series-title":"Logics and Models of Concurrent Systems","article-title":"In transition from global to modular temporal reasoning about programs","author":"Pnueli","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1055","series-title":"Proc. 17th IEEE Symp. on Foundations of Comp. Sci. (FOCS'76)","first-page":"109","article-title":"Semantical considerations on Floyd-Hoare logic","author":"Pratt","year":"1976"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1060","series-title":"Proc. Ann. ACM Symp. on Foundations of Computer Science (FOCS '81)","article-title":"A decidable \u00b5-calculus","author":"Pratt","year":"1981"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1065","series-title":"Past, Present and Future","author":"Prior","year":"1967"},{"key":"10.1016\/B978-044450813-3\/50026-6_rf1075","series-title":"Time and Modality","author":"Prior","year":"1957"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1075","series-title":"Proc. 5th Int. Symp. on Programming","article-title":"Specification and verification of concurrent systems in CESAR","author":"Quielle","year":"1981"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1080","article-title":"Fairness and related properties in transition systems","author":"Quielle","year":"1982","journal-title":"Technical Report 292, IMAG"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1085","first-page":"1","article-title":"Decidability of second order theories and automata on infinite trees","volume":"141","author":"Rabin","year":"1969","journal-title":"Trans. AMS"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1090","series-title":"Elements of Distributed Algorithms","author":"Reisig","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1095","series-title":"Temporal Logic","author":"Rescher","year":"1971"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1100","series-title":"Proc. IEEE\/ACM Int. Conf. on Computer Aided Design (ICCAD '93)","first-page":"42","article-title":"Dynamic variable reordering for ordered binary decision diagrams","author":"Rudell","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1105","series-title":"Proc. 29th IEEE Symp. on Foundations of Computer Science (FOCS '88)","article-title":"On the complexity of omega-automata","author":"Safra","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1110","first-page":"227","article-title":"Formalized algorithmic languages","volume":"18","author":"Salwicki","year":"1970","journal-title":"Bull. Acad. Polon. Sci., Ser. Sci. Math. Astron. Phys."},{"issue":"2","key":"10.1016\/B978-044450813-3\/50026-6_bb1115","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1080\/11663081.1992.10510780","article-title":"Expressive completeness of temporal logic of trees","volume":"2","author":"Schlingloff","year":"1992","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1120","series-title":"Proc. 2nd Int. Symp. Logical Foundations of Computer Science (\u201cLogic at Tver\u201d)","first-page":"441","article-title":"On the expressive power of modal logic on trees","author":"Schlingloff","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1125","first-page":"27","article-title":"Verification of finite-state systems with temporal logic model checking","volume":"19","author":"Schlingloff","year":"1997","journal-title":"South African Computer Journal"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1130","series-title":"\u2018Relational Methods in Computer Science\u2019, Advances in Computing Science","article-title":"Relational algebra and modal logics","author":"Schlingloff","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1135","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1111\/j.1755-2567.1968.tb00335.x","article-title":"Decidability of S4.1","volume":"34","author":"Segerberg","year":"1968","journal-title":"Theoria"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1140","article-title":"An essay in classical modal logic","author":"Segerberg","year":"1971","journal-title":"Technical Report Filosofiska Studier 13, Department of Philosophy, University of Uppsala"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1145","article-title":"Theoretical Issues in the Design and Verification of Distributed Systems","author":"Sistla","year":"1983","journal-title":"PhD thesis, CMU Dept. of Computer Science"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50026-6_bb1150","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","article-title":"Complexity of propositional temporal logics","volume":"32","author":"Sistla","year":"1986","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1155","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","article-title":"The complementation problem for B\u00fcchi automata with applications to temporal logic","volume":"49","author":"Sistla","year":"1987","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50026-6_bb1160","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1023\/A:1008629725384","article-title":"Stubborn sets for real-time Petri nets","volume":"11","author":"Sloan","year":"1997","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1165","series-title":"A system for determining propositional logic theorems by applying values and rules to triplets that are generated from a formula","author":"Stlmarck","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1170","series-title":"Proc. Int. Conf. on Safety of Computer Control Systems (SAFECOMP '90)","first-page":"31","article-title":"Modelling and verifying systems and software in propositional logic","author":"Stlmarck","year":"1990"},{"issue":"4\/5","key":"10.1016\/B978-044450813-3\/50026-6_bb1175","first-page":"293","article-title":"Reachability analysis of Petri nets using symmetries","volume":"8","author":"Starke","year":"1991","journal-title":"Syst. Anal. Model. Simul."},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1180","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1016\/0304-3975(87)90012-0","article-title":"Modal logics for communicating systems","volume":"49","author":"Stirling","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1185","series-title":"Handbook of Logic in Computer Science","article-title":"Modal and temporal logics","author":"Stirling","year":"1991"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50026-6_bb1190","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1016\/0304-3975(90)90110-4","article-title":"Local model checking in the modal \u00b5-calculus","volume":"89","author":"Stirling","year":"1991","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1195","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","article-title":"Depth first search and linear graph algorithms","volume":"1","author":"Tarjan","year":"1972","journal-title":"SIAM Journal of Computing"},{"key":"10.1016\/B978-044450813-3\/50026-6_rf1205","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","article-title":"A lattice-theoretical fixpoint theorem and its applications","volume":"5","author":"Tarski","year":"1955","journal-title":"Pacific J. Math."},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1205","series-title":"Proc. 12th Ann. IEEE Symp. on Logic in Computer Science (LICS '97)","first-page":"183","article-title":"An expressively complete linear time temporal logic for Mazurkiewicz traces","author":"Thiagarajan","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1210","article-title":"Automata on infinite objects","volume":"Vol. B","author":"Thomas","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1215","first-page":"389","article-title":"Languages, automata, and logic","volume":"Vol. III","author":"Thomas","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1220","series-title":"Proc. 1991 Int. Workshop on Formal Methods in VLSI Design","article-title":"Testing language containment for ?-automata using BDDs","author":"Touati","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1225","series-title":"Proc. 2nd Workshop on Computer Aided Verification (CAV '90)","first-page":"156","article-title":"A stubborn attack on state explosion","author":"Valmari","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1230","series-title":"Modal Logic and Classical Logic","author":"van Benthem","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1235","series-title":"Handbook of Philosophical Logic","first-page":"167","article-title":"Correspondence theory","author":"van Benthem","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1240","series-title":"The Logic of Time","author":"van Benthem","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1245","series-title":"Computer Science Today: Recent Trends and Developments","article-title":"Alternating automata and program verification","author":"Vardi","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1250","series-title":"Proc. 14th Int. ACM Symp. on the Theory of Computing","first-page":"137","article-title":"The complexity of relational query languages","author":"Vardi","year":"1982"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1255","series-title":"Proc. 1st Symp. on Logic in Computer Science (LICS '86)","article-title":"An automata-theoretic approach to automatic program verification","author":"Vardi","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1260","series-title":"Proc. 10th Ann. IEEE Symp. on Logic in Computer Science (LICS '95)","first-page":"14","article-title":"Completeness of Kozen's axiomatisation of the propositional \u00b5-calculus","author":"Walukiewicz","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1265","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1016\/0304-3975(91)90043-2","article-title":"A note on model checking the modal ?-calculus","volume":"83","author":"Winskel","year":"1991","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1270","series-title":"Proc. 9th Int. Symp. on Principles of Programming Languages (POPL '82)","first-page":"20","article-title":"Specification and synthesis of communicating processes using an extended temporal logic","author":"Wolper","year":"1982"},{"issue":"1\u20132","key":"10.1016\/B978-044450813-3\/50026-6_bb1275","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","article-title":"Temporal logic can be more expressive","volume":"56","author":"Wolper","year":"1983","journal-title":"Information and Control"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1280","first-page":"119","article-title":"The tableau method for temporal logic: An overview","volume":"110\u2013111","author":"Wolper","year":"1985","journal-title":"Logique et Analyse"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1285","series-title":"Proc. 13th ACM Symp. on Principles of Programming Languages (POPL '86)","article-title":"Expressing interesting properties of programs in propositional temporal logic","author":"Wolper","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1290","series-title":"Proc. Int. Workshop on Automatic Verification Methods for Finite State Systems","article-title":"Verifying properties of large sets of processes with network invariants","author":"Wolper","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1295","series-title":"Proc. IEEE Symp. on Research in Security and Privacy","article-title":"A semantic model for authentication protocols","author":"Woo","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1300","series-title":"Proc. of 19th Int. Symp. on Fault-tolerant Computing","first-page":"134","article-title":"A fast timing verification method based on the independence of units","author":"Yoneda","year":"1989"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50026-6_bb1305","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1023\/A:1008682131325","article-title":"Efficient verification of parallel real-time systems","volume":"11","author":"Yoneda","year":"1997","journal-title":"Formal Methods in System Design"},{"issue":"1\/2","key":"10.1016\/B978-044450813-3\/50026-6_bb1310","article-title":"Kronos: A verification tool for real-time systems","volume":"1","author":"Yovine","year":"1997","journal-title":"Software Tools for Technology Transfer"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1315","series-title":"Embedded Systems","article-title":"Model-checking timed automata","author":"Yovine","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50026-6_bb1320","series-title":"Proc. Int. Conf. on Automated Deduction (CADE '97)","first-page":"272","article-title":"SATO: An efficient propositional prover","author":"Zhang","year":"1997"}],"container-title":["Handbook of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500266?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500266?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T00:55:35Z","timestamp":1556499335000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444508133500266"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9780444508133"],"references-count":264,"URL":"https:\/\/doi.org\/10.1016\/b978-044450813-3\/50026-6","relation":{},"subject":[],"published":{"date-parts":[[2001]]}}}