{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T06:53:39Z","timestamp":1760079219280},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649878"},{"type":"electronic","value":"9783540498018"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055145","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T09:09:13Z","timestamp":1153991353000},"page":"331-348","source":"Crossref","is-referenced-by-count":9,"title":["I\/O automata and beyond: Temporal logic and abstraction in Isabelle"],"prefix":"10.1007","author":[{"given":"Olaf","family":"M\u00fcller","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"M. Archer and C. Heitmeyer. Human-style theorem proving using PVS. In E. Gunter, editor, Proc. 10th Int. Conf. on Theorem Proving in Higher Order Logics (TPHOL'97), volume 1275 of Lecture Notes in Computer Science, pages 33\u201348. Springer-Verlag, 1997.","DOI":"10.1007\/BFb0028384"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"A. Biere. \u039ccke \u2014 Efficient \u039c-calculus model checking. In O. Grumberg, editor, Proc. 9th Int. Conf. on Computer Aided Verification, volume 1254 of Lecture Notes in Computer Science, pages 468\u2013471. Springer-Verlag, 1997.","DOI":"10.1007\/3-540-63166-6_50"},{"key":"20_CR3","unstructured":"N. Bj\u00d8rner, A. Browne, E. Chang, M. Col\u00f3n, A. Kapur, Z. Manna, H. B. Sipma, and T. E. Uribe. STeP: deductive-algorithmic verification of reactive and real-time systems. In R. Alur and T. A. Henzinger, editors, Computer Aided Verification: 8th International Conference, volume 1102 of Lecture Notes in Computer Science, pages 415\u2013418. Springer-Verlag, 1996."},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"M. Devillers, D. Griffioen, and O. M\u00fcller. Possibly infinite sequences in theorem provers: A comparative study. In E. Gunter, editor, Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOL'97), volume 1275 of Lecture Notes in Computer Science, pages 89\u2013104. Springer-Verlag, 1997.","DOI":"10.1007\/BFb0028388"},{"key":"20_CR5","volume-title":"Technical Report MIT\/LCS\/TR-587","author":"R. Gawlick","year":"1993","unstructured":"R. Gawlick, R. Segala, J. Sogaard-Andersen, and N. Lynch. Liveness in timed and untimed systems. Technical Report MIT\/LCS\/TR-587, Laboratory for Computer Science, MIT, Cambridge, MA, December 1993."},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"F. Kr\u00f6ger. Temporal Logic of Programs. Springer-Verlag, 1987.","DOI":"10.1007\/978-3-642-71549-5"},{"issue":"3","key":"20_CR7","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"L. Lamport. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, 16(3):872\u2013923, May 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"T. L\u00e5ngbacka. A HOL formalisation of the Temporal Logic of Actions. In T. Melham and J. Camilleri, editors, Proc. 7th Int. Workshop on Higher Order Logic Theorem Provers and Applications, volume 859 of Lecture Notes in Computer Science, pages 332\u2013347. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58450-1_52"},{"key":"20_CR9","unstructured":"N. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, 1996."},{"key":"20_CR10","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, NY, 1995."},{"key":"20_CR11","unstructured":"S. Merz. Mechanizing TLA in Isabelle. In Workshop Verification in New Orientations, 1995. Technical Report, University Maribor."},{"key":"20_CR12","unstructured":"O. M\u00fcller. Abstraction rules for I\/O automata using temporal logic. 1998. in preparation."},{"key":"20_CR13","unstructured":"O. M\u00fcller. A Verification Environment for I\/O Automata based on formalized Meta-Theory. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00c4t M\u00fcnchen, 1998."},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"O. M\u00fcller and T. Nipkow. Combining model checking and deduction for I\/O-automata. In Proc. 1st Workshop Tools and Algorithms for the Construction and Analysis of Systems, volume 1019 of Lecture Notes in Computer Science, pages 1\u201316. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60630-0_1"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"O. M\u00fcller and T. Nipkow. Traces of I\/O-automata in Isabelle\/HOLCF. In Proc. 7th Int. Joint Conf. on Theory and Practice of Software Development (TAPSOFT'97), volume 1214 of Lecture Notes in Computer Science, pages 580\u2013595. Springer-Verlag, 1997.","DOI":"10.1007\/BFb0030627"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"O. M\u00fcller, T. Nipkow, D. Oheimb, and O. Slotosch. HOLCF = HOL + LCF. J. Functional Programming, 1998. submitted.","DOI":"10.1017\/S095679689900341X"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"J. F. Soegaard-Andersen, S. J. Garland, J. V. Guttag, N. A. Lynch, and A. Pogosyants. Computer-assisted simulation proofs. In C. Courcoubetis, editor, Proc. 5th Int. Conf. Computer-Aided Verificatio (CAV'93), volume 697 of Lecture Notes in Computer Science, pages 305\u2013319. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56922-7_25"},{"key":"20_CR19","unstructured":"J. Wright. Mechanising the Temporal Logic of Actions in HOL. In M. Archer, J. Joyce, K. Levitt, and P. Windley, editors, Proc. 1991 Int. Workshop on the HOL Theorem Proving System and its Applications, pages 155\u2013159. IEEE Computer Society Press, 1992."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055145","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,20]],"date-time":"2019-04-20T08:34:24Z","timestamp":1555749264000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055145"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0055145","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}