{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:56:46Z","timestamp":1779087406931,"version":"3.51.4"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1995,1]]},"DOI":"10.1007\/bf01384313","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T03:30:13Z","timestamp":1112412613000},"page":"11-44","source":"Crossref","is-referenced-by-count":238,"title":["Property preserving abstractions for the verification of concurrent systems"],"prefix":"10.1007","volume":"6","author":[{"given":"C.","family":"Loiseaux","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Graf","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.","family":"Sifakis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Bouajjani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Bensalem","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Probst","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings.Theoretical Computer Science, 82 (2), 1991. First published as Report SRC-29, DEC Research Center in 1988.","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, S. Bensalem, C. Loiseaux, and J. Sifakis. Property preserving simulations. InWorkshop on Computer-Aided Verification (CAV), Montr\u00e9al. LNCS 630, June 1992.","DOI":"10.1007\/3-540-56496-9_21"},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, J.-C. Fernandez, S. Graf, J. Sifakis, and C. Rodriguez, ?Safety for branching semantics,? In18th ICALP, Madrid. LNCS 510, Springer Verlag, 1991.","DOI":"10.1007\/3-540-54233-7_126"},{"key":"CR4","unstructured":"A. Bouajjani, ?From Linear-Time Propositional Temporal Logics to a Branching-Time ?-calculus,? RTC 15, LGI-IMAG, Grenoble, 1989."},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"R. E. Bryant, ?Graph based algorithms for boolean function manipulation,?IEEE Trans. on Computation, 35 (8), 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"CR6","unstructured":"J. R. B\u00fcchi, ?On a decision method in restricted second order arithmetic,? InInternational Congress on Logic, Method and Philosophical Science. Stanford University Press, 1962."},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot, ?Systematic design of program analysis framework,? InProc. 6th ACM Symp. on Principle of Programming Languages, 1979.","DOI":"10.1145\/567752.567778"},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation. PLILP'92, LNCS 631, pp. 269?295. Springer Verlag.","DOI":"10.1007\/3-540-55844-6_142"},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, E. A. Emerson, and E. Sistla, ?Automatic verification of finite state concurrent systems using temporal logic specification: a practical approach,? In10th ACM Symposium on Principles of Programming Languages (POPL83). Complete version published in ACM TOPLAS, 8(2):244?263, April 1986.","DOI":"10.1145\/5397.5399"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, O. Grumberg, and D. E. Long, ?Model checking and abstraction,? InSymposium on Principles of Programming Languages (POPL 92). ACM, January 1992.","DOI":"10.1145\/143165.143235"},{"key":"CR11","volume-title":"Parallel Program Design","author":"K.M. Chandy","year":"1988","unstructured":"K.M. Chandy and J. Misra,Parallel Program Design. Addison-Wesley, Massachusetts, 1988."},{"key":"CR12","unstructured":"D. Dams, O. Grumberg, and R. Gerth, ?Abstract interpretation of reactive systems: Abstractions preserving ?CTL*, ?CTL* and CTL*,?IFIP Conference PROCOMET' 94."},{"key":"CR13","series-title":"Technical Report T90006","volume-title":"Specification and validation of a simple overtaking protocol using LOTOS","author":"P. Ernberg","year":"1990","unstructured":"P. Ernberg, L. Fredlund, and B. Jonsson, ?Specification and validation of a simple overtaking protocol using LOTOS,? Technical Report T90006, SICS, Sweden, 1990."},{"key":"CR14","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and J.Y. Halpern, ??Sometimes? and ?not never? revisited: On branching versus linear time,? In10th ACM Symposium on Principles of Programming Languages (POPL 83). Published in Journal of ACM, 33:151?178.","DOI":"10.1145\/4904.4999"},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"O. Grumberg and E. Long, ?Compositionnal model checking and modular verification,? In J.C.M. Baeten and J.F. Groote, editors,Concur'91, pp. 250?265. LNCS 527, Springer-Verlag, 1991.","DOI":"10.1007\/3-540-54430-5_93"},{"key":"CR16","unstructured":"S. Graf and C. Loiseaux, ?Program verification using compositional abstraction,? InTAPSOFT 93, joint conference CAAP\/FASE. LNCS 668, Springer Verlag, April 1993."},{"key":"CR17","doi-asserted-by":"crossref","unstructured":"S. Graf and C. Loiseaux, ?A tool for symbolic program verification and abstraction,? InConference on Computer Aided Verification CAV'93, Heraklion Crete. LNCS 697, Springer Verlag, 1993.","DOI":"10.1007\/3-540-56922-7_7"},{"key":"CR18","doi-asserted-by":"crossref","unstructured":"S. Graf, ?Verification of a distributed cache memory by using abstractions,?Conference on Computer Aided Verification CAV'94, Stanford. LNCS 818, Springer Verlag, 1994.","DOI":"10.1007\/3-540-58179-0_55"},{"key":"CR19","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare.Communicating Sequential Processes. Prentice Hall International, 1984.","DOI":"10.1007\/978-3-662-09507-2_19"},{"key":"CR20","unstructured":"ISO. IS ISO\/OSI 8807-LOTOS: a formal description technique based on the temporal ordering of observational behaviour. International standard, ISO, 1989."},{"key":"CR21","doi-asserted-by":"crossref","unstructured":"H. Jifeng, ?Various simulations and refinements?, InREX Workshop on Stepwise Refinement of Distributed Systems, Mook. LNCS 430, Springer Verlag, 1989.","DOI":"10.1007\/3-540-52559-9_70"},{"key":"CR22","doi-asserted-by":"crossref","unstructured":"B. Jonsson, ?On decomposing and refining specifications of distributed systems,? InREX Workshop on Stepwise Refinement of Distributed Systems, Mook. LNCS 430, Springer Verlag, 1989.","DOI":"10.1007\/3-540-52559-9_71"},{"key":"CR23","unstructured":"J. Katzenelson and B. Kurshan, ?S\/R: A Language for Specifying Protocols and other Coordinating Processes,? In5th Ann. Int'l Phoenix Conf. Comput. Commun., pp. 286?292. IEEE, 1986."},{"key":"CR24","doi-asserted-by":"crossref","unstructured":"D. Kozen, ?Results on the propositional ?-calculus?, InTheoretical Computer Science. North-Holland, 1983.","DOI":"10.7146\/dpb.v11i146.7420"},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan, ?Analysis of discrete event coordination,? InREX Workshop on Stepwise Refinement of Distributed Systems, Mook. LNCS 430, Springer Verlag, 1989.","DOI":"10.1007\/3-540-52559-9_74"},{"key":"CR26","unstructured":"L. Lamport, ?The temporal logic of actions?, Technical Report 79, DEC, Systems Research Center, 1991."},{"key":"CR27","unstructured":"C. Loiseaux, V\u00e9rification symbolique de programmes r\u00e9actifs \u00e0 l'aide d'abstractions. Thesis, Universit\u00e9 Joseph Fourier, Grenoble, February 1994."},{"key":"CR28","volume-title":"An introduction to Input\/Output automata","author":"N.A. Lynch","year":"1988","unstructured":"N.A. Lynch and M.R. Tuttle, ?An introduction to Input\/Output automata,? Report MIT\/LCS\/TM 373, MIT, Cambridge, Massachussetts, November 1988."},{"key":"CR29","unstructured":"R. Milner, ?An algebraic definition of simulation between programs,? InProc. Second Int. Joint Conf. on Artificial Intelligence, pp. 481?489. BCS, 1971."},{"key":"CR30","doi-asserted-by":"crossref","unstructured":"R. Milner, ?A calculus of communication systems? InLNCS 92. Springer Verlag, 1980.","DOI":"10.1007\/3-540-10235-3"},{"key":"CR31","doi-asserted-by":"crossref","unstructured":"R. Milner, ?A calculus for Synchrony and Asynchrony,?Journal of Theoretical Computer Science, 25, 1983.","DOI":"10.1016\/0304-3975(83)90114-7"},{"key":"CR32","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli, ?A hierarchy of temporal properties,? InProceedings of 9th ACM Symposium on Principles of Distributed Computing, 1990.","DOI":"10.1145\/93385.93442"},{"key":"CR33","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1090\/S0002-9947-1944-0010555-7","volume":"55","author":"O. Ore","year":"1944","unstructured":"O. Ore, ?Galois connexions,?Trans. Amer. Math. Soc, 55:493?513, February 1944.","journal-title":"Trans. Amer. Math. Soc"},{"key":"CR34","doi-asserted-by":"crossref","unstructured":"A. Pnueli, ?The Temporal Logic of Programs,? In18th Symposium on Foundations of Computer Science (FOCS 77). IEEE, 1977. Revised version published in Theoretical Computer Science, 13:45?60, 1981.","DOI":"10.1016\/0304-3975(81)90110-9"},{"key":"CR35","doi-asserted-by":"crossref","unstructured":"A. Pnueli, ?Application of temporal logic to specification and verification of reactive systems: a survey of current trends,? InCurrent trends in Concurrency, Nordwijkerhout. LNCS 224, Springer Verlag, 1986.","DOI":"10.1007\/BFb0027047"},{"key":"CR36","unstructured":"J.P. Queille. Le syst\u00e8me CESAR: Description, sp\u00e9cification et analyse des applications r\u00e9parties. Thesis, Universit\u00e9 Scientifique et M\u00e9dicale de Grenoble, June 1982."},{"key":"CR37","doi-asserted-by":"crossref","unstructured":"Luis E. Sanchis, ?Data types as lattices: retractions, closures and projections,? InRAIRO Theorical computer science, vol 11, no. 4, pp. 339?344, 1977.","DOI":"10.1051\/ita\/1977110403291"},{"key":"CR38","volume-title":"Property preserving homomorphisms and a notion of simulation of transition systems","author":"J. Sifakis","year":"1982","unstructured":"J. Sifakis, ?Property preserving homomorphisms and a notion of simulation of transition systems,? RR 332, IMAG, Grenoble, November 1982."},{"key":"CR39","unstructured":"J. Sifakis, ?Property preserving homomorphisms of transition systems,? In E. Clarke and D. Kozen, editors,4th Workshop on Logics of Programs, Pittsburgh. LNCS 164, Springer Verlag, June 1983."},{"key":"CR40","doi-asserted-by":"crossref","unstructured":"P. Wolper, ?Temporal logic can be more expressive,?Information and Control, 56, 1983.","DOI":"10.1016\/S0019-9958(83)80051-5"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384313.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01384313\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384313","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T16:25:21Z","timestamp":1586190321000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01384313"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,1]]},"references-count":40,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1995,1]]}},"alternative-id":["BF01384313"],"URL":"https:\/\/doi.org\/10.1007\/bf01384313","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,1]]}}}