{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:06:28Z","timestamp":1761620788167,"version":"3.43.0"},"reference-count":63,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2000,6,1]],"date-time":"2000-06-01T00:00:00Z","timestamp":959817600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,6,1]],"date-time":"2000-06-01T00:00:00Z","timestamp":959817600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2000,6]]},"DOI":"10.1023\/a:1008700623084","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T11:37:32Z","timestamp":1040557052000},"page":"227-270","source":"Crossref","is-referenced-by-count":50,"title":["Verifying Temporal Properties of Reactive Systems: A STeP Tutorial"],"prefix":"10.1007","volume":"16","author":[{"given":"Nikolaj S.","family":"Bj\u00f8rner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anca","family":"Browne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael A.","family":"Col\u00f3n","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zohar","family":"Manna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Henny B.","family":"Sipma","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom\u00e1s E.","family":"Uribe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"260864_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur and T.A. Henzinger (Eds.), Proc. 8th Intl. Conference on Computer Aided Verification. LNCS, Vol. 1102, Springer-Verlag, July 1996.","DOI":"10.1007\/3-540-61474-5"},{"key":"260864_CR2","first-page":"187","volume":"1166","author":"C. Barrett","year":"1996","unstructured":"C. Barrett, D.L. Dill, and J. Levitt, \u201cValidity checking for combinations of theories with equality, \u201d in 1st Intl. Conf. on Formal Methods in Computer-Aided Design. LNCS, Vol. 1166, Nov. 1996, pp. 187\u2013201.","journal-title":"1st Intl. Conf. on Formal Methods in Computer-Aided Design"},{"key":"260864_CR3","doi-asserted-by":"crossref","unstructured":"S. Bensalem, Y. Lakhnech, and S. Owre, \u201cComputing abstractions of infinite state systems compositionally and automatically, \u201d in A.J. Hu and M.Y. Vardi (Eds.), Proc. 10th Intl. Conferance on Computer Aided Verification. LNCS, Vol. 1427, Springer-Verlag, June 1998, pp. 319\u2013331.","DOI":"10.1007\/BFb0028755"},{"key":"260864_CR4","doi-asserted-by":"crossref","unstructured":"S. Bensalem, Y. Lakhnech, and H. Saidi, \u201cPowerful techniques for the automatic generation of invariants, \u201d in R. Alur and T.A. Henzinger (Eds.), Proc. 8th Intl. Conferance on Computer Aided Verification. LNCS, Vol. 1102, Springer-Verlag, July 1996, pp. 323\u2013335.","DOI":"10.1007\/3-540-61474-5_80"},{"key":"260864_CR5","unstructured":"N.S. Bj\u00f8rner, \u201cIntegrating decision procedures for temporal verification, \u201d PhD Thesis, Computer Science Department, Stanford University, Nov. 1998."},{"key":"260864_CR6","unstructured":"N.S. Bj\u00f8rner, A. Browne, E.S. Chang, M. Col\u00f3n, A. Kapur, Z. Manna, H.B. Sipma, and T.E. Uribe, \u201cSTeP: The Stanford Temporal Prover, \u201d User's Manual, Technical Report STAN-CS-TR-95-1562, Computer Science Department, Stanford University, Nov. 1995."},{"key":"260864_CR7","doi-asserted-by":"crossref","unstructured":"N.S. Bj\u00f8rner, A. Browne, E.S. Chang, M. Col\u00f3n, A. Kapur, Z. Manna, H.B. Sipma, and T.E. Uribe, \u201cSTeP: Deductive-algorithmic verification of reactive and real-time systems, \u201d in R. Alur and T.A. Henzinger (Eds.), Proc. 8th Intl. Conference on Computer Aided Verification. LNCS, Vol. 1102, Springer-Verlag, July 1996, pp. 415\u2013418.","DOI":"10.1007\/3-540-61474-5_92"},{"issue":"1","key":"260864_CR8","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/S0304-3975(96)00191-0","volume":"173","author":"N.S. Bj\u00f8rner","year":"1997","unstructured":"N.S. Bj\u00f8rner, A. Browne, and Z. Manna, \u201cAutomatic generation of invariants and intermediate assertions, \u201d Theoretical Computer Science, Vol. 173, No. 1, pp. 49\u201387, February 1997. Preliminary version appeared in 1st Intl. Conf. on Principles and Practice of Constraint Programming, LNCS, Vol. 976, Springer-Verlag, 1995, pp. 589-623.","journal-title":"Theoretical Computer Science"},{"key":"260864_CR9","unstructured":"N.S. Bj\u00f8rner, U. Lerner, and Z. Manna, \u201cDeductive verification of parameterized fault-tolerant systems: A case study, \u201d in Proc. Intl. Conf. on Temporal Logic, Kluwer."},{"key":"260864_CR10","first-page":"484","volume":"1231","author":"N.S. Bj\u00f8rner","year":"1998","unstructured":"N.S. Bj\u00f8rner, Z. Manna, H.B. Sipma, and T.E. Uribe, \u201cDeductive verification of real-time systems using STeP, \u201d Technical Report STAN-CS-TR-98-1616, Stanford University, Jan. 1998. To appear in Theoretical Computer Science. Preliminary version appeared in 4th Intl. AMASTWorkshop on Real-Time Systems, LNCS, Vol. 1231, Springer-Verlag, May 1997, pp. 484\u2013498.","journal-title":"Theoretical Computer Science"},{"key":"260864_CR11","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1007\/3-540-63104-6_13","volume":"1249","author":"N.S. Bj\u00f8rner","year":"1997","unstructured":"N.S. Bj\u00f8rner, M.E. Stickel, and T.E. Uribe, \u201cA practical integration of first-order reasoning and decision procedures, \u201d in Proc. of the 14th Intl. Conference on Automated Deduction. LNCS, Vol. 1249, Springer-Verlag, July 1997, pp. 101\u2013115.","journal-title":"Proc. of the 14th Intl. Conference on Automated Deduction"},{"key":"260864_CR12","unstructured":"E. B\u00f6rger (Ed.), Specification and Validation Methods, Oxford University Press, International Schools for Computer Scientists, 1994."},{"key":"260864_CR13","unstructured":"E. B\u00f6rger, Y. Gurevich, and D. Rosenzweig, \u201cThe Bakery algorithm: Yet another specification and veri-fication, \u201d in E. B\u00f6rger (Ed.), Specification and Validation Methods, Oxford University Press, International Schools for Computer Scientists, 1994, pp. 231\u2013243."},{"key":"260864_CR14","first-page":"83","volume":"11","author":"R.S. Boyer","year":"1988","unstructured":"R.S. Boyer and J.S. Moore, \u201cIntegrating decision procedures into heuristic theorem provers: A case study with linear arithmetic, \u201d Machine Intelligence, Vol. 11, pp. 83\u2013124, 1988.","journal-title":"Machine Intelligence"},{"issue":"1","key":"260864_CR15","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1016\/0304-3975(92)90183-G","volume":"96","author":"J.C. Bradfield","year":"1992","unstructured":"J.C. Bradfield and C. Stirling, \u201cLocal model checking for infinite state spaces, \u201d Theoretical Computer Science, Vol. 96, No. 1, pp. 157\u2013174, Apr. 1992.","journal-title":"Theoretical Computer Science"},{"key":"260864_CR16","doi-asserted-by":"crossref","first-page":"484","DOI":"10.1007\/3-540-60692-0_69","volume":"1026","author":"A. Browne","year":"1995","unstructured":"A. Browne, Z. Manna, and H.B. Sipma, \u201cGeneralized temporal verification diagrams, \u201d in 15th Conference on the Foundations of Software Technology and Theoretical Computer Science. LNCS, Vol. 1026, Springer-Verlag, 1995, pp. 484\u2013498.","journal-title":"15th Conference on the Foundations of Software Technology and Theoretical Computer Science"},{"issue":"8","key":"260864_CR17","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant, \u201cGraph-based algorithms for Boolean function manipulation, \u201d IEEE Transactions on Computers, Vol. C-35, No. 8, pp. 677\u2013691, Aug. 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"260864_CR18","doi-asserted-by":"crossref","unstructured":"E.S. Chang, Z. Manna, and A. Pnueli, \u201cCharacterization of temporal property classes, \u201d in W. Kuich (Ed.), Proc. 19th Intl. Colloq. Aut. Lang. Prog. LNCS, Vol. 623, Springer-Verlag, 1992, pp. 474\u2013486.","DOI":"10.1007\/3-540-55719-9_97"},{"key":"260864_CR19","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0025774","volume":"131","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E.A. Emerson, \u201cDesign and synthesis of synchronization skeletons using branching time temporal logic, \u201d in Proc. IBM Workshop on Logics of Programs. LNCS, Vol. 131, Springer-Verlag, 1981, pp. 52\u201371.","journal-title":"Proc. IBM Workshop on Logics of Programs"},{"issue":"5","key":"260864_CR20","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"E.M. Clarke, O. Grumberg, and D.E. Long, \u201cModel checking and abstraction, \u201d ACM Trans. on Programming Languages and Systems, Vol. 16, No. 5, pp. 1512\u20131542, Sept. 1994.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"260864_CR21","doi-asserted-by":"crossref","unstructured":"M.A. Col\u00f3n and T.E. Uribe, \u201cGenerating finite-state abstractions of reactive systems using decision procedures, \u201d in A.J. Hu and M.Y. Vardi (Eds.), in Proc. 10th Intl. Conference on Computer Aided Verification. LNCS, Vol. 1427, Springer-Verlag, 1998, pp. 293\u2013304.","DOI":"10.1007\/BFb0028753"},{"key":"260864_CR22","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot, \u201cAbstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, \u201d in 4th ACM Symp. Princ. of Prog. Lang., ACM Press, 1977, pp. 238\u2013252.","DOI":"10.1145\/512950.512973"},{"key":"260864_CR23","doi-asserted-by":"crossref","unstructured":"P. Cousot and N. Halbwachs, \u201cAutomatic discovery of linear restraints among the variables of a program, \u201d in 5th ACM Symp. Princ. of Prog. Lang., Jan. 1978.","DOI":"10.1145\/512760.512770"},{"key":"260864_CR24","unstructured":"D.R. Dams, \u201cAbstract interpretation and partition refinement for model checking, \u201d PhD Thesis, Eindhoven University of Technology, July 1996."},{"key":"260864_CR25","unstructured":"D.L. Detlefs, K.R.M. Leino, G. Nelson, and J.B. Saxe, \u201cExtended static checking, \u201d Technical Report 159, Compaq SRC, Dec. 1998."},{"issue":"3","key":"260864_CR26","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1093\/logcom\/6.3.343","volume":"6","author":"L. Fix","year":"1996","unstructured":"L. Fix and O. Grumberg, \u201cVerification of temporal properties, \u201d J. Logic and Computation, Vol. 6, No. 3, pp. 343\u2013362, 1996.","journal-title":"J. Logic and Computation"},{"issue":"1","key":"260864_CR27","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1109\/TSE.1975.6312821","volume":"1","author":"S.M. German","year":"1975","unstructured":"S.M. German and B. Wegbreit, \u201cA synthesizer of inductive assertions, \u201d IEEE transactions on Software Engineering, Vol. 1, No. 1, pp. 68\u201375, March 1975.","journal-title":"IEEE transactions on Software Engineering"},{"key":"260864_CR28","unstructured":"M. Gordon and T.F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, 1993."},{"key":"260864_CR29","doi-asserted-by":"crossref","unstructured":"S. Graf and H. Saidi, \u201cConstruction of abstract state graphs with PVS, \u201d in O. Grumberg (Ed.), Proc. 9th Intl. Conference on Computer Aided Verification. LNCS, Vol. 1254, Springer-Verlag, June 1997, pp. 72\u201383.","DOI":"10.1007\/3-540-63166-6_10"},{"key":"260864_CR30","doi-asserted-by":"crossref","unstructured":"R. Hardin, Z. Har'El, and R. Kurshan, \u201cCOSPAN, \u201d in R. Alur and T.A. Henzinger (Eds.), Proc. 8th Intl. Conference on Computer Aided Verification. LNCS, Vol. 1102, Springer-Verlag, July 1996, pp. 423\u2013427.","DOI":"10.1007\/3-540-61474-5_94"},{"key":"260864_CR31","doi-asserted-by":"crossref","unstructured":"G.J. Holzmann and D. Peled, \u201cThe state of SPIN, \u201d In R. Alur and T.A. Henzinger (Eds.), Proc. 8th Intl. Conference on Computer Aided Verification. LNCS, Vol. 1102, Springer-Verlag, July 1996, pp. 385\u2013389.","DOI":"10.1007\/3-540-61474-5_85"},{"key":"260864_CR32","unstructured":"A.J. Hu and M.Y. Vardi (Eds.), Proc. 10th Intl. Conference on Computer Aided Verification. LNCS, Vol. 1427, Springer-Verlag, June 1998."},{"key":"260864_CR33","doi-asserted-by":"crossref","unstructured":"Y. Kesten, Z. Manna, and A. Pnueli, \u201cTemporal verification of simulation and refinement, \u201d in J.W. de Bakker, C. Huizing, W.-P. de Roever, and G. Rosenberg (Eds.), \u201cA Decade of Concurrency: Reflections and Perspectives,\u201d LNCS, Vol. 803, Springer-Verlag, 1994, pp. 273\u2013346.","DOI":"10.1007\/3-540-58043-3_22"},{"key":"260864_CR34","doi-asserted-by":"crossref","unstructured":"Y. Kesten, Z. Manna, and A. Pnueli, \u201cVerifying clocked transition systems, \u201d in R. Alur, T.A. Henzinger, and E.D. Sontag (Eds.), Hybrid Systems III, LNCS, Vol. 1066, Springer-Verlag, 1996, pp. 13\u201340.","DOI":"10.1007\/BFb0020933"},{"key":"260864_CR35","unstructured":"R.P. Kurshan, \u201cTesting containment of \u03c9-regular languages, \u201d Technical Report 1121-861010-33, Bell Labs, 1986."},{"key":"260864_CR36","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan, Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach, Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"issue":"8","key":"260864_CR37","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1145\/361082.361093","volume":"17","author":"L. Lamport","year":"1974","unstructured":"L. Lamport, \u201cA new solution of Dijkstra's concurrent programming problem, \u201d Communications of the ACM, Vol. 17, No. 8, pp. 435\u2013455, 1974.","journal-title":"Communications of the ACM"},{"issue":"1","key":"260864_CR38","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/BF00265219","volume":"7","author":"L. Lamport","year":"1976","unstructured":"L. Lamport, \u201cThe synchronization of independent processes, \u201d Acta Informatica, Vol. 7, No. 1, pp. 15\u201334, 1976.","journal-title":"Acta Informatica"},{"issue":"3","key":"260864_CR39","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"L. Lamport, \u201cThe temporal logic of actions, \u201d ACM Transactions on Programming Languages and Systems, Vol. 16, No. 3, pp. 872\u2013923, May 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"260864_CR40","series-title":"Research Report","volume-title":"Should your specification language be typed?","author":"L. Lamport","year":"1997","unstructured":"L. Lamport and L.C. Paulson, \u201cShould your specification language be typed?\u201d Research Report 147, DEC Systems Research Center, Palo Alto, CA, May 1997."},{"key":"260864_CR41","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem, \u201cProperty preserving abstractions for the verification of concurrent systems, \u201d Formal Methods in System Design, Vol. 6, pp. 1\u201335, 1995.","journal-title":"Formal Methods in System Design"},{"key":"260864_CR42","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Anuchitanukul, N. Bj\u00f8rner, A. Browne, E.S. Chang, M. Col\u00f3n, L. de Alfaro, H. Devarajan, H.B. Sipma, and T.E. Uribe, \u201cSTeP: The Stanford temporal prover, \u201d Technical Report STAN-CS-TR-94-1518, Computer Science Department, Stanford University, July 1994.","DOI":"10.21236\/ADA324036"},{"key":"260864_CR43","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Browne, H.B. Sipma, and T.E. Uribe, \u201cVisual abstractions for temporal verification, \u201d in A. Haeberer (Ed.), Algebraic Methodology and Software Technology (AMAST'98), LNCS, Vol. 1548, Springer-Verlag, Dec. 1998, pp. 28\u201341.","DOI":"10.1007\/3-540-49253-4_5"},{"key":"260864_CR44","doi-asserted-by":"crossref","unstructured":"Z. Manna, M.A. Col\u00f3n, B. Finkbeiner, H.B. Sipma, and T.E. Uribe, \u201cAbstraction and modular verification of infinite-state reactive systems, \u201d in M. Broy (Ed.), Requirements Targeting Software and Systems Engineering (RTSE). LNCS, Vol. 1526, Springer-Verlag, 1997, pp. 273\u2013292.","DOI":"10.1007\/10692867_13"},{"issue":"1","key":"260864_CR45","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z. Manna","year":"1991","unstructured":"Z. Manna and A. Pnueli, \u201cCompleting the temporal picture, \u201d Theoretical Computer Science, Vol. 83, No. 1, pp. 97\u2013130, 1991.","journal-title":"Theoretical Computer Science"},{"key":"260864_CR46","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1991","unstructured":"Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, New York, 1991."},{"key":"260864_CR47","doi-asserted-by":"crossref","first-page":"609","DOI":"10.1007\/BF01191722","volume":"30","author":"Z. Manna","year":"1993","unstructured":"Z. Manna and A. Pnueli, \u201cModels for reactivity, \u201d Acta Informatica, Vol. 30, pp. 609\u2013678, 1993.","journal-title":"Acta Informatica"},{"key":"260864_CR48","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli, \u201cTemporal verification diagrams, \u201d in M. Hagiya and J.C. Mitchell (Eds.), Proc. International Symposium on Theoretical Aspects of Computer Software. LNCS, Vol. 789, Springer-Verlag, 1994, pp. 726\u2013765.","DOI":"10.1007\/3-540-57887-0_123"},{"key":"260864_CR49","unstructured":"Z. Manna and A. Pnueli, \u201cVerification of parameterized programs, \u201d in B\u00f6rger (Ed.), Specification and Validation Methods, Oxford University Press, International Schools for Computer Scientists, 1994, pp. 167\u2013230."},{"key":"260864_CR50","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Z. Manna and A. Pnueli, Temporal Verification of Reactive Systems: Safety, Springer-Verlag, New York, 1995."},{"key":"260864_CR51","doi-asserted-by":"crossref","unstructured":"Z. Manna and H.B. Sipma, \u201cDeductive verification of hybrid systems using STeP, \u201d in T. Henzinger and S. Sastry (Eds.), Hybrid Systems: Computation and Control. LNCS, Vol. 1386, Springer-Verlag, Apr. 1998, pp. 305\u2013318.","DOI":"10.1007\/3-540-64358-3_47"},{"key":"260864_CR52","first-page":"25","volume":"1633","author":"Z. Manna","year":"1999","unstructured":"Z. Manna and H.B. Sipma, \u201cVerification of parameterized systems by dynamic induction on diagrams, \u201d in Proc. 11th Intl. Conference on Computer Aided Verification. LNCS, Vol. 1633, Springer-Verlag, 1999, pp. 25\u201343.","journal-title":"Proc. 11th Intl. Conference on Computer Aided Verification"},{"key":"260864_CR53","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, Symbolic Model Checking, Kluwer Academic Pub., 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"issue":"2","key":"260864_CR54","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"G. Nelson and D.C. Oppen, \u201cFast decision procedures based on congruence closure, \u201d J. ACM, Vol. 27, No. 2, pp. 356\u2013364, Apr. 1980.","journal-title":"J. ACM"},{"key":"260864_CR55","doi-asserted-by":"crossref","unstructured":"S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas, \u201cPVS: Combining specification, proof checking, and model checking, \u201d in R. Alur and T.A. Henzinger (Eds.), in Proc. 8th Intl. Conference on Computer Aided Verification. LNCS, Vol. 1102, Springer-Verlag, July 1996, pp. 411\u2013414.","DOI":"10.1007\/3-540-61474-5_91"},{"key":"260864_CR56","doi-asserted-by":"crossref","unstructured":"A. Pnueli, \u201cThe temporal logic of programs, \u201d in Proc. 18th IEEE Symp. Found. of Comp. Sci., IEEE Computer Society Press, 1977, pp. 46\u201357.","DOI":"10.1109\/SFCS.1977.32"},{"key":"260864_CR57","unstructured":"A. Pnueli, \u201cLecture notes: the Bakery algorithm, \u201d Draft Manuscript, Weizmann Institute of Science, Israel, May 1996."},{"key":"260864_CR58","doi-asserted-by":"crossref","unstructured":"J. Queille and J. Sifakis, \u201cSpecification and verification of concurrent systems in CESAR, \u201d in M. Dezani-Ciancaglini and U. Montanari (Eds.), Intl. Symposium on Programming. LNCS, Vol. 137, Springer-Verlag, 1982, pp. 337\u2013351.","DOI":"10.1007\/3-540-11494-7_22"},{"issue":"1","key":"260864_CR59","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R.E. Shostak","year":"1984","unstructured":"R.E. Shostak, \u201cDeciding combinations of theories, \u201d J. ACM, Vol. 31. No. 1, pp. 1\u201312, Jan. 1984.","journal-title":"J. ACM"},{"key":"260864_CR60","unstructured":"H.B. Sipma, \u201cDiagram-based verification of discrete, real-time and hybrid systems, \u201d Ph.D. Thesis, Computer Science Department, Stanford University, Feb. 1999."},{"key":"260864_CR61","doi-asserted-by":"crossref","unstructured":"W. Thomas, \u201cAutomata on infinite objects, \u201d in J. van Leeuwen (Ed.), Handbook of Theoretical Computer Science, Vol. B, Elsevier Science Publishers (North-Holland), 1990, pp. 133\u2013191.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"260864_CR62","unstructured":"T.E. Uribe, \u201cAbstraction-based deductive-algorithmic verification of reactive systems, \u201d PhD Thesis, Computer Science Department, Stanford University, Dec. 1998. Technical Report STAN-CS-TR-99-1618."},{"key":"260864_CR63","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M.Y. Vardi","year":"1986","unstructured":"M.Y. Vardi and P. Wolper, \u201cAutomata-theoretic techniques for modal logics of programs, \u201d J. Comp. Sys. Sci., Vol. 32, pp. 183\u2013221, 1986.","journal-title":"J. Comp. Sys. Sci."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008700623084.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008700623084\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008700623084.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T04:12:30Z","timestamp":1754367150000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008700623084"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,6]]},"references-count":63,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2000,6]]}},"alternative-id":["260864"],"URL":"https:\/\/doi.org\/10.1023\/a:1008700623084","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2000,6]]}}}