{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T06:57:36Z","timestamp":1648969056357},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1993,2,1]],"date-time":"1993-02-01T00:00:00Z","timestamp":728524800000},"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":[[1993,2]]},"DOI":"10.1007\/bf01383942","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T02:05:31Z","timestamp":1112407531000},"page":"7-43","source":"Crossref","is-referenced-by-count":2,"title":["Modular abstractions for verifying real-time distributed systems"],"prefix":"10.1007","volume":"2","author":[{"given":"Hana","family":"De-Leon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Orna","family":"Grumberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","unstructured":"R. Alur and T.A. Henzinger. A really temporal logic. 30th IEEE FOCS, 1989.","DOI":"10.1109\/SFCS.1989.63473"},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. 5th IEEE LICS, 1990.","DOI":"10.1007\/3-540-54233-7_128"},{"key":"CR3","unstructured":"R. Alur. Techniques for automatic verification of real-time systems. Ph.D. thesis, Stanford University, 1991."},{"key":"CR4","unstructured":"E.A. Emerson, A.K. Mok, A.P. Sistla, and J. Srinivasan. Quantitative temporal reasoning.Workshop on Automatic Verification Methods for Finite-State Systems, Grenoble, France, 1989."},{"key":"CR5","unstructured":"E. Harel. Temporal analysis of real-time systems. M.S. thesis, Weizmann Institute, 1988."},{"key":"CR6","unstructured":"E. Harel, O. Lichtenstein, and A. Pnueli. Explicit clock temporal logic. 5th IEEE LICS, 1990."},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"R. Alur and T.A. Henzinger. Logics and models of real time: a survey. REX, 1991.","DOI":"10.1007\/BFb0031988"},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan. analysis of discrete event coordination, stepwise refinement of distributed systems. Lecture Notes in Computer Science,Conference Record of the 12th Annual ACM Symposium on Principles of Programming Languages, New Orleans, LA, January, 1985. 430: 414?453 (1990).","DOI":"10.1007\/3-540-52559-9_74"},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"G. Shurek and O. Grumberg. The modular framework of computer-aided verification.Workshop on Computer Aided Verification, Rutgers, NJ, June 1990.","DOI":"10.1090\/dimacs\/003\/23"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"O. Grumberg and D.E. Long. Model checking and modular verification.CONCUR, Amsterdam, August 1991.","DOI":"10.1007\/3-540-54430-5_93"},{"key":"CR11","unstructured":"X. Nicollin and J. Sifakis. The algebra of timed processes ATP: theory and application. IMAG, RT-C26, December 1990."},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"R. Alur and T.A. Henzinger. Real time logics: complexity and expressiveness. 5th IEEE LICS, 1990.","DOI":"10.21236\/ADA323441"},{"key":"CR13","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M.C. Browne","year":"1988","unstructured":"M.C. Browne, E.M. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59:115?131 (1988).","journal-title":"Theoretical Computer Science"},{"key":"CR14","doi-asserted-by":"crossref","unstructured":"C. Stirling and D.J. Walker. Local model checking in the modal mu-calculus. TAPSOFT89, March 1989.","DOI":"10.1007\/3-540-50939-9_144"},{"key":"CR15","doi-asserted-by":"crossref","first-page":"725","DOI":"10.1007\/BF00264284","volume":"27","author":"R. Cleaveland","year":"1990","unstructured":"R. Cleaveland, Tableau-based model checking in the propositional mu-calculus.Acta Informatica, 27:725?747 (1990).","journal-title":"Acta Informatica"},{"key":"CR16","unstructured":"J. Bradfield and C. Stirling. Local model checking for infinite state spaces.Workshop on Computer Aided Verification, Aalborg, Denmark, July 1991."},{"key":"CR17","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/BF01667079","volume":"2","author":"A.U. Shankar","year":"1987","unstructured":"A.U. Shankar and S.S. Lam. Time-dependent distributed systems: proving safety, liveness and real-time properties.Distributed Computing, 2:61?79 (1987).","journal-title":"Distributed Computing"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383942.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01383942\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383942","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T16:22:41Z","timestamp":1586190161000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01383942"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,2]]},"references-count":17,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1993,2]]}},"alternative-id":["BF01383942"],"URL":"https:\/\/doi.org\/10.1007\/bf01383942","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,2]]}}}