{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:23:30Z","timestamp":1725665010980},"publisher-location":"Berlin, Heidelberg","reference-count":58,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540653066"},{"type":"electronic","value":"9783540494423"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-65306-6_24","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:42:52Z","timestamp":1330299772000},"page":"643-681","source":"Crossref","is-referenced-by-count":7,"title":["Distributed versions of linear time temporal logic: A trace perspective"],"prefix":"10.1007","author":[{"given":"P. S.","family":"Thiagarajan","sequence":"first","affiliation":[]},{"given":"Jesper G.","family":"Henriksen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Alur, R., Peled, D., Penczek, W.: Model checking of causality properties. Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press (1995) 90\u2013100","key":"12_CR1","DOI":"10.1109\/LICS.1995.523247"},{"unstructured":"Bell Labs Design Automation: FormalChecktm. Further information can be obtained at http:\/\/www.bell-labs.com\/formalcheck\/","key":"12_CR2"},{"issue":"1-2","key":"12_CR3","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/S0304-3975(96)00012-6","volume":"174","author":"F. Bracho","year":"1997","unstructured":"Bracho, F., Droste, M., Kuske, D.: Representation of computations in concurrent automata by dependence orders. Theoretical Computer Science 174(1-2) (1997) 67\u201396","journal-title":"Theoretical Computer Science"},{"unstructured":"B\u00fcchi, J. R.: On a decision method in restricted second order arithmetic. Proceedings of the International Congress on Logic, Methodology and Philosophy of Science, Stanford University Press (1960) 1\u201311","key":"12_CR4"},{"doi-asserted-by":"crossref","unstructured":"Cheng, A.: Petri nets, traces, and local model checking. Proceedings of the 4th International Conference on Algebraic Methodology and Software Technology, Lecture Notes in Computer Science 936, Springer-Verlag (1995) 322\u2013337","key":"12_CR5","DOI":"10.1007\/3-540-60043-4_62"},{"doi-asserted-by":"crossref","unstructured":"Diekert, V.: Combinatorics of traces. Lecture Notes in Computer Science 454, Springer-Verlag (1990)","key":"12_CR6","DOI":"10.1007\/3-540-53031-2"},{"doi-asserted-by":"crossref","unstructured":"Diekert, V., Rozenberg, G. (eds.): The book of traces. World Scientific (1995)","key":"12_CR7","DOI":"10.1142\/2563"},{"issue":"1","key":"12_CR8","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0304-3975(94)00266-L","volume":"150","author":"M. Droste","year":"1995","unstructured":"Droste, M.: Recognizable languages in concurrency monoids. Theoretical Computer Science 150(1) (1995) 77\u2013109","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"Droste, M., Gastin, P.: Asynchronous cellular automata for pomsets without auto-concurrency. Proceedings of the 7th International Conference on Concurrency Theory, Lecture Notes in Computer Science 1119, Springer-Verlag (1996) 627\u2013638","key":"12_CR9","DOI":"10.1007\/3-540-61604-7_80"},{"unstructured":"Ebinger, W.: Charakterisierung von sprachklassen unendlicher spuren durch logiken. Dissertation, Institut f\u00fcr Informatik, Universit\u00e4t Stuttgart (1994)","key":"12_CR10"},{"issue":"1","key":"12_CR11","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0304-3975(95)00130-1","volume":"154","author":"W. Ebinger","year":"1996","unstructured":"Ebinger, W., Muscholl, A.: Logical definability on infinite traces. Theoretical Computer Science 154(1) (1996) 67\u201384","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"Emerson, A. E.: Temporal and modal logic. In Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, Elsevier Science Publishers (1990) 996\u20131072","key":"12_CR12","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"issue":"2","key":"12_CR13","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M. J. Fischer","year":"1979","unstructured":"Fischer, M. J., Ladner, R. E.: Propositional dynamic logic of regular programs. Journal of Computer and System Sciences 18(2) (1979) 194\u2013211","journal-title":"Journal of Computer and System Sciences"},{"doi-asserted-by":"crossref","unstructured":"Gabbay, A., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. Proceedings of the 7th Annual Symposium on Principles of Programming Languages, ACM (1980) 163\u2013173","key":"12_CR14","DOI":"10.1145\/567446.567462"},{"doi-asserted-by":"crossref","unstructured":"Gastin, P., Petit, A.: Asynchronous cellular automata for infinite traces. Proceedings of the 19th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science 623, Springer-Verlag (1992) 583\u2013594","key":"12_CR15","DOI":"10.1007\/3-540-55719-9_106"},{"doi-asserted-by":"crossref","unstructured":"Gerth, R., Kuiper, R., Peled, D., Penczek, W.: A partial-order approach to branching time model checking. Proceedings of the 3rd Israeli Symposium on Theory of Computing and Systems, IEEE Computer Society Press (1995) 130\u2013139","key":"12_CR16","DOI":"10.1109\/ISTCS.1995.377038"},{"doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Partial-order methods for the verification of concurrent systems. Lecture Notes in Computer Science 1032, Springer-Verlag (1996)","key":"12_CR17","DOI":"10.1007\/3-540-60761-7"},{"doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple on-the-fly automatic verification of linear time temporal logic. Proceedings of the 15th IFIP WG 6.1 International Workshop on Protocol Specification, Testing, and Verification, North-Holland (1995)","key":"12_CR18","DOI":"10.1007\/978-0-387-34892-6_1"},{"unstructured":"Henriksen, J. G., Thiagarajan, P. S.: Dynamic linear time temporal logic. Journal of Pure and Applied Logic, Elsevier (to appear)","key":"12_CR19"},{"doi-asserted-by":"crossref","unstructured":"Henriksen, J. G., Thiagarajan, P. S.: A product version of dynamic linear time temporal logic. Proceedings of the 8th International Conference on Concurrency Theory, Lecture Notes in Computer Science 1243, Springer-Verlag (1997) 45\u201358","key":"12_CR20","DOI":"10.1007\/3-540-63141-0_4"},{"unstructured":"Holzmann, G. J.: An overview of the SPIN model checker. In \u201cOn-the-fly Model Checking Tutorial\u201d, BRIGS Autumn School on Verification, Note NS-96-6, BRICS, Department of Computer Science, University of Aarhus (1996)","key":"12_CR21"},{"key":"12_CR22","series-title":"Technical Report","volume-title":"On semantic and logical refinement of actions","author":"M. Huhn","year":"1996","unstructured":"Huhn, M.: On semantic and logical refinement of actions. Technical Report, Institut f\u00fcr Informatik, Universit\u00e4t Hildesheim, Germany (1996)"},{"unstructured":"Kamp, H. R.: Tense logic and the theory of linear order. Ph.D. thesis, University of California (1968)","key":"12_CR23"},{"issue":"3","key":"12_CR24","first-page":"21","volume":"73","author":"S. Katz","year":"1992","unstructured":"Katz, S., Peled, D.: Interleaving set temporal logic. Theoretical Computer Science 73(3) (1992) 21\u201343","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"12_CR25","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1006\/inco.1995.1078","volume":"119","author":"K. Lodaya","year":"1995","unstructured":"Lodaya, K., Parikh, R., Ramanujam, R., Thiagarajan, P. S.: A logical study of distributed transition systems. Information and Computation 119(1) (1995) 91\u2013118","journal-title":"Information and Computation"},{"doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems (specification), Springer-Verlag (1991)","key":"12_CR26","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"12_CR27","series-title":"Technical report DAIMI PB-78","volume-title":"Concurrent program schemes and their interpretations","author":"A. Mazurkiewicz","year":"1977","unstructured":"Mazurkiewicz, A.: Concurrent program schemes and their interpretations. Technical report DAIMI PB-78, Department of Computer Science, University of Aarhus, Denmark (1977)"},{"doi-asserted-by":"crossref","unstructured":"Meyer, R., Petit, A.: Expressive completeness of LTrL on finite traces: an algebraic proof. Proceedings of the 15th Annual Symposium on Theoretical Aspects of Computer Science 1373, Lecture Notes in Computer Science, Springer-Verlag (1998) 533\u2013543","key":"12_CR28","DOI":"10.1007\/BFb0028588"},{"issue":"3","key":"12_CR29","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/s004460050031","volume":"10","author":"M. Mukund","year":"1997","unstructured":"Mukund, M., Sohoni, M.: Keeping track of the latest gossip in a distributed system. Distributed Computing 10(3) (1997) 117\u2013127","journal-title":"Distributed Computing"},{"doi-asserted-by":"crossref","unstructured":"Mukund, M., Thiagarajan, P. S.: Linear time temporal logics over Mazurkiewicz traces. Proceedings of the 21st International Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science 1113, Springer-Verlag (1996) 62\u201392","key":"12_CR30","DOI":"10.1007\/3-540-61550-4_140"},{"doi-asserted-by":"crossref","unstructured":"Niebert, P.: A \u03bd-calculus with local views for systems of sequential agents. Proceedings of the 20th International Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science 969, Springer-Verlag (1995) 563\u2013573","key":"12_CR31","DOI":"10.1007\/3-540-60246-1_161"},{"unstructured":"Niebert, P.: A temporal logic for the specification and validation of distributed behaviour. Ph.D. thesis, University of Hildesheim (1997)","key":"12_CR32"},{"issue":"1","key":"12_CR33","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0304-3975(81)90112-2","volume":"13","author":"M. Nielsen","year":"1981","unstructured":"Nielsen, M., Plotkin, G., Winskel, G.: Petri nets, event structures and domains, part I. Theoretical Computer Science 13(1) (1981) 85\u2013108","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"12_CR34","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/0304-3975(94)90009-4","volume":"126","author":"D. Peled","year":"1994","unstructured":"Peled, D., Pnueli, A.: Proving partial order properties. Theoretical Computer Science 126(2) (1994) 143\u2013182","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"Peled, D.: Partial order reduction: model checking using representatives. Proceedings of the 21st International Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science 1113, Springer-Verlag (1996) 93\u2013112","key":"12_CR35","DOI":"10.1007\/3-540-61550-4_141"},{"issue":"1","key":"12_CR36","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1142\/S0129054193000043","volume":"4","author":"W. Penczek","year":"1993","unstructured":"Penczek, W.: Temporal logics for trace systems: on automated verification. International Journal of the Foundations of Computer Science 4(1) (1993) 31\u201368","journal-title":"International Journal of the Foundations of Computer Science"},{"doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. Proceedings of the 18th Annual Symposium on Foundations of Computer Science, IEEE Computer Society Press (1977) 46\u201357","key":"12_CR37","DOI":"10.1109\/SFCS.1977.32"},{"doi-asserted-by":"crossref","unstructured":"Ramanujam, R.: Locally linear time temporal logic. Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press (1996) 118\u2013127","key":"12_CR38","DOI":"10.1109\/LICS.1996.561311"},{"doi-asserted-by":"crossref","unstructured":"Ramanujam, R.: Rules for trace consistent reasoning. Proceedings of the 3rd Asian Computing Science Conference, Lecture Notes in Computer Science 1345, Springer-Verlag (1997) 57\u201371","key":"12_CR39","DOI":"10.1007\/3-540-63875-X_43"},{"doi-asserted-by":"crossref","unstructured":"Reisig, W.: Temporal logic and causality in concurrent systems. Proceedings of CONCURRENCY'88, Lecture Notes in Computer Science 335, Springer-Verlag (1988) 121\u2013139","key":"12_CR40","DOI":"10.1007\/3-540-50403-6_37"},{"doi-asserted-by":"crossref","unstructured":"Reisig, W.: Petri net models for distributed algorithms. In Computer Science Today \u2014 Recent Trends and Developments, Lecture Notes in Computer Science 1000, Springer-Verlag (1995) 441\u2013454","key":"12_CR41","DOI":"10.1007\/BFb0015259"},{"issue":"3","key":"12_CR42","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A. P. Sistla","year":"1985","unstructured":"Sistla, A. P., Clarke, E.: The complexity of propositional linear temporal logics. Journal of the ACM 32(3) (1985) 733\u2013749","journal-title":"Journal of the ACM"},{"key":"12_CR43","volume-title":"The complexity of decision problems in automata theory and logic","author":"L. J. Stockmeyer","year":"1974","unstructured":"Stockmeyer, L. J.: The complexity of decision problems in automata theory and logic. Ph.D. thesis, MIT, Cambridge, Massachusetts (1974)"},{"doi-asserted-by":"crossref","unstructured":"Thiagarajan, P. S.: A trace based extension of linear time temporal logic. Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press (1994) 438\u2013447","key":"12_CR44","DOI":"10.1109\/LICS.1994.316047"},{"key":"12_CR45","series-title":"Technical report TCS-93-6","volume-title":"TrPTL: a trace based extension of linear time temporal logic","author":"P. S. Thiagarajan","year":"1993","unstructured":"Thiagarajan, P. S.: TrPTL: a trace based extension of linear time temporal logic. Technical report TCS-93-6, School of Mathematics, SPIC Science Foundation, Madras (1993)"},{"doi-asserted-by":"crossref","unstructured":"Thiagarajan, P. S.: A trace consistent subset of PTL. Proceedings of the 6th International Conference on Concurrency Theory, Lecture Notes in Computer Science 962, Springer-Verlag (1995) 438\u2013452","key":"12_CR46","DOI":"10.1007\/3-540-60218-6_33"},{"key":"12_CR47","series-title":"Technical report TCS-95-4","volume-title":"PTL over product state spaces","author":"P. S. Thiagarajan","year":"1995","unstructured":"Thiagarajan, P. S.: PTL over product state spaces. Technical report TCS-95-4, School of Mathematics, SPIC Science Foundation, Madras (1995)"},{"doi-asserted-by":"crossref","unstructured":"Thiagarajan, P. S., Walukiewicz, I.: An expressively complete linear time temporal logic for Mazurkiewicz traces. Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press (1997) 183\u2013194","key":"12_CR48","DOI":"10.1109\/LICS.1997.614946"},{"unstructured":"homas, W.: Automata on infinite objects. In Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, Elsevier Science Publishers (1990) 133\u2013191","key":"12_CR49"},{"key":"12_CR50","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/BF00709154","volume":"1","author":"A. Valmari","year":"1992","unstructured":"Valmari, A.: A stubborn attack on state explosion. Formal Methods in Systems Design 1 (1992) 285\u20133131","journal-title":"Formal Methods in Systems Design"},{"unstructured":"Vardi, M. Y., Wolper, P.: An automata-theoretic approach to automatic program verification. Proceedings of the 1st Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press (1986) 332\u2013345","key":"12_CR51"},{"doi-asserted-by":"crossref","unstructured":"Vardi, M. Y.: An automata-theoretic approach to linear time temporal logic. In Logics for Concurrency \u2014 Structure vs. Automata, Lecture Notes in Computer Science 1043, Springer-Verlag (1996) 238\u2013266","key":"12_CR52","DOI":"10.1007\/3-540-60915-6_6"},{"unstructured":"Walukiewicz, I.: Difficult configurations \u2014 on the complexity of LTrL (extended abstract). Proceedings of the 25th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, Springer-Verlag (to appear)","key":"12_CR53"},{"doi-asserted-by":"crossref","unstructured":"Willems, B., Wolper, P.: Partial-order methods for model checking: from linear time to branching time. Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press (1996) 294\u2013303","key":"12_CR54","DOI":"10.1109\/LICS.1996.561357"},{"unstructured":"Winskel, G., Nielsen, M.: Models for concurrency. In Handbook of Logic and the Foundations of Computer Science, volume 4, Oxford University Press (1995) 1\u2013148","key":"12_CR55"},{"doi-asserted-by":"crossref","unstructured":"Wolper, P.: Temporal logic can be more expressive. Proceedings of the 22nd Annual IEEE Symposium on Foundations of Computer Science, IEEE Computer Society Press (1981) 340\u2013348","key":"12_CR56","DOI":"10.1109\/SFCS.1981.44"},{"doi-asserted-by":"crossref","unstructured":"Wolper, P., Vardi, M. Y., Sistla, A. P.: Reasoning about infinite computation paths. Proceedings of the 24th Annual IEEE Symposium on Foundations of Computer Science, IEEE Computer Society Press (1983) 185\u2013194.","key":"12_CR57","DOI":"10.1109\/SFCS.1983.51"},{"key":"12_CR58","first-page":"99","volume":"21","author":"W. Zielonka","year":"1987","unstructured":"Zielonka, W.: Notes on finite asynchronous automata. R.A.I.R.O. Informatique Th\u00e9orique et Applications 21 (1987) 99\u2013135","journal-title":"R.A.I.R.O. Informatique Th\u00e9orique et Applications"}],"container-title":["Lecture Notes in Computer Science","Lectures on Petri Nets I: Basic Models"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-65306-6_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T12:01:04Z","timestamp":1640952064000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-65306-6_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540653066","9783540494423"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/3-540-65306-6_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}