{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T10:15:56Z","timestamp":1649153756032},"publisher-location":"Berlin, Heidelberg","reference-count":51,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540510802","type":"print"},{"value":"9783540461470","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1989]]},"DOI":"10.1007\/bfb0013024","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:06:46Z","timestamp":1132726006000},"page":"201-284","source":"Crossref","is-referenced-by-count":83,"title":["The anchored version of the temporal framework"],"prefix":"10.1007","author":[{"given":"Zohar","family":"Manna","sequence":"first","affiliation":[]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and L. Lamport, The existence of refinement mappings, Proc. 3rd IEEE Symp. Logic in Comp. Sci., 1988, pp. 165\u2013175.","DOI":"10.1109\/LICS.1988.5115"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"B. Alpern and F.B. Schneider, Defining liveness, Info. Proc. Lett. 21, 1985.","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"5_CR3","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B. Alpern","year":"1987","unstructured":"B. Alpern and F.B. Schneider, Recognizing safety and liveness, Distributed Computing 2, 1987, pp. 117\u2013126.","journal-title":"Distributed Computing"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"B. Alpern and F.B. Schneider, Verifying temporal properties without temporal logic, ACM Trans. Prog. Lang. Syst. 11, 1989.","DOI":"10.1145\/59287.62028"},{"key":"5_CR5","series-title":"Mathematical Center Tracts","volume-title":"Correctness preserving program refinements: Proof theory and applications","author":"R.J.R. Back","year":"1980","unstructured":"R.J.R. Back, Correctness preserving program refinements: Proof theory and applications, Mathematical Center Tracts, 131, Center for Mathematics and Computer Science (CWI), Amsterdam, 1980."},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"R.J.R Back and R. Kurki-Suonio, Decentralization of process nets with a centalized control, Proc. 2nd ACM Symp. Princ. of Dist. Comp., 1983, pp. 131\u2013142.","DOI":"10.1145\/800221.806716"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"H. Barringer, R. Kuiper, and A Pnueli, Now you may compose temporal logic specifications, Proc. 16th ACM Symp. Theory of Comp., 1984, pp. 51\u201363.","DOI":"10.1145\/800057.808665"},{"key":"5_CR8","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/BF01257083","volume":"20","author":"M. Ben-Ari","year":"1983","unstructured":"M. Ben-Ari, Z. Manna, and A Pnueli, The temporal logic of branching time, Acta Informatica 20, 1983, pp. 207\u2013226.","journal-title":"Acta Informatica"},{"key":"5_CR9","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla, Automatic verification of finite state concurrent systems using temporal logic specifications, ACM Trans. Prog. Lang. Syst. 8, 1986, pp. 244\u2013263.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"K.M. Chandy and J Misra, Parallel Program Design, Addison-Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"5_CR11","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"E.W. Dijkstra, A Discipline of Programming, Prentice-Hall, New Jersey, 1976."},{"key":"5_CR12","unstructured":"W.P. de Roever and J. Zwiers, Different Styles of Compositional and Modular Proof-systems for a CCS\/CSP-like Language, Technical Report, Philips Research, 1987."},{"key":"5_CR13","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"E.A. Emerson and J.Y. Halpern, 'sometimes\u2019 and \u2018not never\u2019 revisited: On branching time versus linear time, J. ACM 33, 1986, pp. 151\u2013178.","journal-title":"J. ACM"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi, On the temporal analysis of fairness, Proc. 6th ACM Symp. Princ. of Prog. Lang., 1980, pp. 163\u2013173.","DOI":"10.1145\/567446.567462"},{"key":"5_CR15","doi-asserted-by":"crossref","volume-title":"The Science of Programming","author":"D. Gries","year":"1981","unstructured":"D. Gries, The Science of Programming, Springer, New-York, 1981.","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"5_CR16","volume-title":"Compositional Verification of Distributed Systems","author":"B. Jonsson","year":"1987","unstructured":"B. Jonsson, Compositional Verification of Distributed Systems, Ph.D. thesis, Uppsala University, Sweden, 1987."},{"key":"5_CR17","unstructured":"J.A.W. Kamp, Tense Logic and the Theory of Order, Ph.D. thesis, UCLA, 1968."},{"key":"5_CR18","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(85)90043-X","volume":"36","author":"M. Kaminski","year":"1985","unstructured":"M. Kaminski, A classification of \u03c9-regular languages, Theor. Comp. Sci. 36, 1985, pp. 217\u2013229.","journal-title":"Theor. Comp. Sci."},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"R. Koymans and W.P. de Roever, Examples of a real-time temporal logic specifications, The Analysis of Concurrent Systems, Springer, 1983, pp. 231\u2013252.","DOI":"10.1007\/3-540-16047-7_50"},{"key":"5_CR20","series-title":"Technical Report","volume-title":"Interleaving Set Temporal Logic","author":"S. Katz","year":"1987","unstructured":"S. Katz and D. Peled, Interleaving Set Temporal Logic, Technical Report 456, Dept. of Computer Science, Technion, Haifa, Israel, 1987."},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"R. Koymans, J. Vytopyl, and W.P. de Roever, Real-time programming and asynchronous message passing, Proc. 2nd ACM Symp. Princ. of Dist. Comp., 1983.","DOI":"10.1145\/800221.806721"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"L. Lamport, Proving the correctness of multiprocess programs, Trans. on Software Engineering 1, 1977.","DOI":"10.1109\/TSE.1977.229904"},{"key":"5_CR23","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1145\/69624.357207","volume":"5","author":"L. Lamport","year":"1983","unstructured":"L. Lamport, Specifying concurrent program modules, ACM Trans. Prog. Lang. Syst. 5, 1983, pp. 190\u2013222.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"5_CR24","unstructured":"L. Lamport, What good is temporal logic, Proc. IFIP Congress (R.E.A. Mason, ed.), North-Holland, 1983, pp. 657\u2013668."},{"key":"5_CR25","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/BF01691063","volume":"4","author":"L.H. Landweber","year":"1969","unstructured":"L.H. Landweber, Decision problems for \u03c9-automata, Mathematical Systems Theory 4, 1969, pp. 376\u2013384.","journal-title":"Mathematical Systems Theory"},{"key":"5_CR26","unstructured":"O. Lichtenstien and A. Pnueli, Checking that finite state concurrent programs satisfy their linear specification, Proc. 10th ACM Symp. Princ. of Prog. Lang., 1984, pp. 97\u2013107."},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"O. Lichtenstien, A. Pnueli, and L. Zuck, The glory of the past, Proc. Conf. Logics of Programs, Lec. Notes in Comp. Sci. 193, Springer, 1985, pp. 196\u2013218.","DOI":"10.1007\/3-540-15648-8_16"},{"key":"5_CR28","unstructured":"Z. Manna, Mathematical Theory of Computation, McGraw-Hill, 1974."},{"key":"5_CR29","unstructured":"R. McNaughton and S. Papert, Counter Free Automata, MIT Press, 1971."},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli, How to cook a temporal proof system for your pet language, Proc. 9th ACM Symp. Princ. of Prog. Lang., 1983, pp. 141\u2013154.","DOI":"10.1145\/567067.567082"},{"key":"5_CR31","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/BFb0036932","volume":"154","author":"Z. Manna","year":"1983","unstructured":"Z. Manna and A. Pnueli, Proving precedence properties: the temporal way, Proc. 10th Int. Colloq. Aut. Lang. Prog., Lec. Notes in Comp. Sci. 154, Springer, 1983, pp. 491\u2013512.","journal-title":"Lec. Notes in Comp. Sci."},{"key":"5_CR32","series-title":"Mathematical Centre Tracts","first-page":"163","volume-title":"Foundations of Computer Science IV, Distributed Systems: Part 2","author":"Z. Manna","year":"1983","unstructured":"Z. Manna and A. Pnueli, Verification of concurrent programs: A temporal proof system, Foundations of Computer Science IV, Distributed Systems: Part 2 (J.W. De-Bakker and J. Van Leuwen, eds.), Mathematical Centre Tracts 159, Center for Mathematics and Computer Science (CWI), Amsterdam, 1983, pp. 163\u2013255."},{"key":"5_CR33","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/0167-6423(84)90003-0","volume":"32","author":"Z. Manna","year":"1984","unstructured":"Z. Manna and A. Pnueli, Adequate proof principles for invariance and liveness properties of concurrent programs, Sci. Comp. Prog. 32, 1984, pp. 257\u2013289.","journal-title":"Sci. Comp. Prog."},{"key":"5_CR34","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli, Specification and verification of concurrent programs by \u2200-automata, Proc. 14th ACM Symp. Princ. of Prog. Lang., 1987, pp. 1\u201312.","DOI":"10.1145\/41625.41626"},{"key":"5_CR35","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1145\/359340.359353","volume":"21","author":"Z. Manna","year":"1978","unstructured":"Z. Manna and R. Waldinger, Is 'sometime\u2019 sometimes better than \u2018always'?: intermitent assertions in proving program correctness, Comm. ACM 21, 1978, pp. 159\u2013172.","journal-title":"Comm. ACM"},{"key":"5_CR36","doi-asserted-by":"crossref","unstructured":"V. Nguyen, D. Gries, and S. Owicki, A model and temporal proof system for network of processes, Proc. 12th ACM Symp. Princ. of Prog. Lang., 1985, pp. 121\u2013131.","DOI":"10.1145\/318593.318624"},{"key":"5_CR37","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S. Owicki","year":"1982","unstructured":"S. Owicki and L. Lamport, Proving liveness properties of concurrent programs, ACM Trans. Prog. Lang. Syst. 4, 1982, pp. 455\u2013495.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"5_CR38","doi-asserted-by":"crossref","first-page":"510","DOI":"10.1007\/BFb0027047","volume":"224","author":"A. Pnueli","year":"1986","unstructured":"A. Pnueli, Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends, Current Trends in Concurrency, Lec. Notes in Comp. Sci. 224, Springer, 1986, pp. 510\u2013584.","journal-title":"Lec. Notes in Comp. Sci."},{"key":"5_CR39","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/BF00265555","volume":"19","author":"J.P. Queille","year":"1983","unstructured":"J.P. Queille and J. Sifakis, Fairness and related properties in transition systems \u2014 A temporal logic to deal with fairness, Acta Informatica 19, 1983, pp. 195\u2013220.","journal-title":"Acta Informatica"},{"key":"5_CR40","doi-asserted-by":"crossref","unstructured":"M.O. Rabin, Automata on Infinite Objects and Churc's Problem, Volume 13 of Regional Conference Series in Mathematics, Amer. Math. Soc., 1972.","DOI":"10.1090\/cbms\/013"},{"key":"5_CR41","unstructured":"W. Reisig, Petri Nets: An Introduction, Volume 4 of EATCS Monographs on Theoretical Computer Science, Springer, 1985."},{"key":"5_CR42","doi-asserted-by":"crossref","unstructured":"A.P. Sistla, On caracterization of safety and liveness properties in temporal logic, Proc. 4th ACM Symp. Princ. of Dist. Comp., 1985, pp. 39\u201348.","DOI":"10.1145\/323596.323600"},{"key":"5_CR43","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/S0019-9958(82)91258-X","volume":"54","author":"R.S. Street","year":"1982","unstructured":"R.S. Street, Propositional dynamic logic with converse, Information and Control 54, 1982, pp. 121\u2013141.","journal-title":"Information and Control"},{"key":"5_CR44","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/S0019-9958(81)90663-X","volume":"48","author":"W. Thomas","year":"1981","unstructured":"W. Thomas, A combinatorial approach to the theory of \u03c9-automata, Inf. and Cont. 48, 1981, pp. 261\u2013283.","journal-title":"Inf. and Cont."},{"key":"5_CR45","doi-asserted-by":"publisher","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, Automata theoretic techniques for modal logics of programs, J. Comp. Sys. Sci. 32, 1986, pp. 183\u2013221.","journal-title":"J. Comp. Sys. Sci."},{"key":"5_CR46","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/S0019-9958(79)90653-3","volume":"43","author":"K. Wagner","year":"1979","unstructured":"K. Wagner, On \u03c9\u2014regular sets, Information and Control 43, 1979, pp. 123\u2013177.","journal-title":"Information and Control"},{"key":"5_CR47","doi-asserted-by":"crossref","unstructured":"J. Widom, D. Gries, and F.B. Schneider, Completeness and incompleteness of trace-based network proof system, Proc. 14th ACM Symp. Princ. of Prog. Lang., 1987, pp. 27\u201338.","DOI":"10.1145\/41625.41628"},{"key":"5_CR48","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"P. Wolper, Temporal logic can be more expressive, Inf. and Cont. 56, 1983, pp. 72\u201399.","journal-title":"Inf. and Cont."},{"key":"5_CR49","unstructured":"L. Zuck, Past Temporal Logic, Ph.D. thesis, Weizmann Institute, 1986."},{"key":"5_CR50","unstructured":"L. Zuck, Manuscript, 1987."},{"key":"5_CR51","unstructured":"J. Zwiers, Compositionality, Concurrency and Partial Correctness: Proof theories for networks of processes and their connection, Ph.D. thesis, University of Eindhoven, The Netherlands, 1988. To appear in the LNCS-series, Springer."}],"container-title":["Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency","Lecture Notes in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0013024","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:23:50Z","timestamp":1586579030000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0013024"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989]]},"ISBN":["9783540510802","9783540461470"],"references-count":51,"URL":"http:\/\/dx.doi.org\/10.1007\/bfb0013024","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"published":{"date-parts":[[1989]]}}}