{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T03:22:45Z","timestamp":1778296965376,"version":"3.51.4"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[1995,7,1]],"date-time":"1995-07-01T00:00:00Z","timestamp":804556800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1995,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>A systematic analysis of trace- and failure-based compositional semantic models for Basic LOTOS is presented. The analysis is motivated by the fact that the weakest known equivalences preserving sufficient information for several typical verification tasks are failure-based, and the weakness of an equivalence can be advantageous for verification. Both the equivalences and the preorders corresponding to the semantic models are covered. The analysis yields in a natural way two compositional semantic models, which are particularly suited for the verification of a general class of liveness properties, a task which cannot be performed with most established models.<\/jats:p>","DOI":"10.1007\/bf01211218","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T22:18:16Z","timestamp":1109369896000},"page":"440-468","source":"Crossref","is-referenced-by-count":44,"title":["Compositional failure-based semantic models for Basic LOTOS"],"prefix":"10.1145","volume":"7","author":[{"given":"Antti","family":"Valmari","sequence":"first","affiliation":[{"name":"Software Systems Laboratory, Tampere University of Technology, Tampere, Finland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martti","family":"Tienari","sequence":"additional","affiliation":[{"name":"University of Helsinki, Department of Computer Science, University of Helsinki, Finland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","volume-title":"CWI Report CS-R8609","author":"Bergstra J. A.","year":"1986"},{"key":"e_1_2_1_2_2_2","unstructured":"Bergstra J. A. Klop J. W. and Olderog E.-R.: Failures without Chaos: A New Process Semantics for Fair Abstraction. In: Formal Description of Programming Concepts III North-Holland 1987 pp. 77\u2013103."},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(87)90085-7"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Bouajjani A. Fernandez J.-C. and Halbwachs N.: Minimal Model generation. In: Computer-Aided Verification '90 (Proceedings of a Workshop) AMS-ACM DIMACS Series in Discrete Mathematics and Theoretical Computer Science Vol. 3 American Mathematical Society 1991 pp. 85\u201391.","DOI":"10.1090\/dimacs\/003\/08"},{"key":"e_1_2_1_2_5_2","unstructured":"Brinksma E.: A Theory for the Derivation of Tests. In: Protocol Specification Testing and Verification VIII North-Holland pp. 63\u201374. Also in: The Formal Description Technique LOTOS North-Holland 1989 pp. 235\u2013247."},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/828.833"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Brookes S. D. and Roscoe A. W.: An Improved Failures Model for Communicating Sequential Processes. In: Proceedings of the NSF-SERC Seminar on Concurrency Lecture Notes in Computer Science 197 Springer-Verlag 1985 pp. 281\u2013305.","DOI":"10.1007\/3-540-15670-4_14"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/167049.167071"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","first-page":"353","DOI":"10.3233\/FI-1990-13308","article-title":"Infinitary Behaviours and Infinitary Observations","author":"Darondeau P.","year":"1990","journal-title":"Fundamenta Informaticae"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90113-0"},{"key":"e_1_2_1_2_11_2","unstructured":"Eloranta J.: Equivalence Concepts and Algorithms for Transition Systems and CCS-like Languages. Licentiate thesis University of Helsinki Department of Computer Science Report C-1991-2 1991."},{"key":"e_1_2_1_2_12_2","volume-title":"Doctoral thesis","author":"Eloranta J.","year":"1994"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Glabbeek R. J.: The Linear Time \u2014 Branching Time Spectrum. In: Proceedings of CONCUR '90 Lecture Notes in Computer Science 458 Springer-Verlag 1990 pp. 278\u2013297.","DOI":"10.1007\/BFb0039066"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Graf S. and Steffen B.: Compositional Minimization of Finite State Processes. In: Computer-Aided Verification '90 ( Proceedings of a Workshop ) AMS-ACM DIMACS Series in Discrete Mathematics and Theoretical Computer Science Vol. 3 American Mathematical Society 1991 pp. 57\u201373.","DOI":"10.1090\/dimacs\/003\/06"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Hoare C. A. R.: Communicating Sequential Processes . Prentice-Hall 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"e_1_2_1_2_16_2","unstructured":"ISO 8807 International Standard: Information processing systems-Open Systems Interconnection \u2014 LOTOS \u2014 A formal description technique based on the temporal ordering of observational behaviour. International Organization for Standardization 1989."},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Kaivola R. and Valmari A.: Using Truth-Preserving Reductions to Improve the Clarity of Kripke-Models. In: Proceedings of CONCUR '91 Lecture Notes in Computer Science 527 Springer-Verlag 1991 pp. 361\u2013375.","DOI":"10.1007\/3-540-54430-5_100"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Kaivola R. and Valmari A.: The Weakest Compositional Semantic Equivalence Preserving Nexttime-less Linear Temporal Logic. In: Proceedings of CONCUR '92 Lecture Notes in Computer Science 630 Springer-Verlag 1992 pp. 207\u2013221.","DOI":"10.1007\/BFb0084793"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90025-D"},{"key":"e_1_2_1_2_20_2","volume-title":"PhD thesis","author":"Leduc G.","year":"1990"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Leduc G.: Failure-based Congruences Unfair Divergences and New Testing Theory. To appear in Protocol Specification Testing and Verification XIV Chapman & Hall 1994.","DOI":"10.1007\/978-0-387-34867-4_17"},{"key":"e_1_2_1_2_22_2","unstructured":"Milner R.: Communication and Concurrency . Prentice-Hall 1989."},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268075"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Pnueli A.: Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends. In: Current Trends in Concurrency Lecture Notes in Computer Science 224 Springer-Verlag 1986 pp. 510\u2013584.","DOI":"10.1007\/BFb0027047"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1109\/26.35374"},{"key":"e_1_2_1_2_26_2","volume-title":"Report A-1992-4","author":"Valmari A.","year":"1992"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Valmari A.: Compositional State Space Generation. In: Advances in Petri Nets 1993 Lecture Notes in Computer Science 674 Springer-Verlag 1993 pp. 427\u2013457. (Earlier version in Proceedings of the 11th International Conference on Application and Theory of Petri Nets Paris 1990 pp. 43\u201362.)","DOI":"10.1007\/3-540-56689-9_54"},{"key":"e_1_2_1_2_28_2","unstructured":"Valmari A.: The Weakest Deadlock-Preserving Congruence. To appear in Information Processing Letters ."},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Valmari A. and Clegg M.: Reduced Labelled Transition Systems Save Verification Effort. In: Proceedings of CONCUR '91 Lecture Notes in Computer Science 527 Springer-Verlag 1991 pp. 526\u2013540.","DOI":"10.1007\/3-540-54430-5_111"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Valmari A. Kemppainen J. Clegg M. and Levanto M.: Putting Advanced Reachability Analysis Techniques Together: the \u201cARA\u201d Tool. In: Proceedings of Formal Methods Europe '93 Lecture Notes in Computer Science 670 Springer-Verlag 1993 pp. 597\u2013616.","DOI":"10.1007\/BFb0024669"},{"key":"e_1_2_1_2_31_2","unstructured":"Valmari A. and Tienari M.: An Improved Failures Equivalence for Finite-State Systems with a Reduction Algorithm. In: Protocol Specification Testing and Verification XI North-Holland 1991 pp. 3\u201318."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211218.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211218\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211218","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:25:18Z","timestamp":1641482718000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211218"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,7]]},"references-count":31,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1995,7]]}},"alternative-id":["10.1007\/BF01211218"],"URL":"https:\/\/doi.org\/10.1007\/bf01211218","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,7]]}}}