{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T22:14:42Z","timestamp":1773958482468,"version":"3.50.1"},"reference-count":53,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2017,6,6]],"date-time":"2017-06-06T00:00:00Z","timestamp":1496707200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S11403-N23"],"award-info":[{"award-number":["S11403-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100009112","name":"Istituto Nazionale di Alta Matematica \u201cFrancesco Severi\u201d","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100009112","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100005758","name":"Universit\u00e0 Politecnica delle Marche","doi-asserted-by":"publisher","award":["RSA-A 2014"],"award-info":[{"award-number":["RSA-A 2014"]}],"id":[{"id":"10.13039\/501100005758","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Distrib. Comput."],"published-print":{"date-parts":[[2018,6]]},"DOI":"10.1007\/s00446-017-0302-6","type":"journal-article","created":{"date-parts":[[2017,6,6]],"date-time":"2017-06-06T10:00:08Z","timestamp":1496743208000},"page":"187-222","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["Parameterized model checking of rendezvous systems"],"prefix":"10.1007","volume":"31","author":[{"given":"Benjamin","family":"Aminof","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tomer","family":"Kotek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sasha","family":"Rubin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3632-3533","authenticated-orcid":false,"given":"Francesco","family":"Spegni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Helmut","family":"Veith","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,6,6]]},"reference":[{"key":"302_CR1","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Rezine, O.: Verification of directed acyclic ad hoc networks. In: Beyer, D., Boreale, M. (eds) Formal Techniques for Distributed Systems: Joint IFIP WG 6.1 International Conference, FMOODS\/FORTE 2013, Held as Part of the 8th International Federated Conference on Distributed Computing Techniques, DisCoTec 2013, Florence, Italy, 3-5 June 2013, Proceedings, pp. 193\u2013208, Springer, Berlin, Heidelberg (2013). doi: 10.1007\/978-3-642-38592-6_14","DOI":"10.1007\/978-3-642-38592-6_14"},{"key":"302_CR2","doi-asserted-by":"crossref","unstructured":"Aminof, B., Jacobs, S., Khalimov, A., Rubin, S.: Parameterized model checking of token-passing systems. In: McMillan, K.L., Rival, X. (eds.) Verification, Model Checking, and Abstract Interpretation\u201415th International Conference, VMCAI 2014, San Diego, CA, USA, January 19\u201321, 2014, Proceedings, Volume 8318 of Lecture Notes in Computer Science, pp. 262\u2013281. Springer (2014)","DOI":"10.1007\/978-3-642-54013-4_15"},{"key":"302_CR3","doi-asserted-by":"crossref","unstructured":"Aminof, B., Kotek, T., Rubin, S., Spegni, F., Veith, H.: Parameterized model checking of rendezvous systems. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014\u2014Concurrency Theory\u201425th International Conference, CONCUR 2014, Rome, Italy, September 2\u20135, 2014. Proceedings, Volume 8704 of Lecture Notes in Computer Science, pp. 109\u2013124. Springer (2014)","DOI":"10.1007\/978-3-662-44584-6_9"},{"key":"302_CR4","doi-asserted-by":"crossref","unstructured":"Aminof, B., Murano, A., Rubin, S., Zuleger, F.: Verification of asynchronous mobile-robots in partially-known environments. In: PRIMA 2015: Principles and Practice of Multi-agent Systems\u201418th International Conference, Bertinoro, Italy, October 26\u201330, 2015, Proceedings, pp. 185\u2013200 (2015)","DOI":"10.1007\/978-3-319-25524-8_12"},{"key":"302_CR5","unstructured":"Aminof, B., Murano, A., Rubin, S., Zuleger, F.: Automatic verification of multi-agent systems in parameterised grid-environments. In: Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems, Singapore, May 9\u201313, 2016, pp. 1190\u20131199 (2016)"},{"key":"302_CR6","doi-asserted-by":"crossref","unstructured":"Aminof, B., Rubin, S.: Model checking parameterised multi-token systems via the composition method. In: Olivetti, N., Tiwari, A. (eds.) Automated Reasoning\u20148th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27\u2013July 2, 2016, Proceedings, Volume 9706 of Lecture Notes in Computer Science, pp. 499\u2013515. Springer (2016)","DOI":"10.1007\/978-3-319-40229-1_34"},{"key":"302_CR7","doi-asserted-by":"crossref","unstructured":"Aminof, B., Rubin, S., Zuleger, F.: On the expressive power of communication primitives in parameterised systems. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning\u201420th International Conference, LPAR-20 2015, Suva, Fiji, November 24\u201328, 2015, Proceedings, Volume 9450 of Lecture Notes in Computer Science, pp. 313\u2013328. Springer (2015)","DOI":"10.1007\/978-3-662-48899-7_22"},{"key":"302_CR8","doi-asserted-by":"crossref","unstructured":"Aminof, B., Rubin, S., Zuleger, F., Spegni, F.: Liveness of parameterized timed networks. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) Automata, Languages, and Programming\u201442nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6\u201310, 2015, Proceedings, Part II, Volume 9135 of Lecture Notes in Computer Science, pp. 375\u2013387. Springer (2015)","DOI":"10.1007\/978-3-662-47666-6_30"},{"issue":"4","key":"302_CR9","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/s00446-007-0040-2","volume":"20","author":"D Angluin","year":"2007","unstructured":"Angluin, D., Aspnes, J., Eisenstat, D., Ruppert, E.: The computational power of population protocols. Distrib. Comput. 20(4), 279\u2013304 (2007)","journal-title":"Distrib. Comput."},{"key":"302_CR10","doi-asserted-by":"crossref","unstructured":"Au\u00dferlechner, S., Jacobs, S., Khalimov, A.: Tight cutoffs for guarded protocols with fairness. In: Jobstmann, B., Leino, K.R.M. (eds.) Verification, Model Checking, and Abstract Interpretation\u201417th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17\u201319, 2016. Proceedings, Volume 9583 of Lecture Notes in Computer Science, pp. 476\u2013494. Springer (2016)","DOI":"10.1007\/978-3-662-49122-5_23"},{"key":"302_CR11","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"302_CR12","doi-asserted-by":"crossref","unstructured":"Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K., Ustuner, A.: Thorough static analysis of device drivers. In: Berbers, Y., Zwaenepoel, W. (eds.) Proceedings of the 2006 EuroSys Conference, Leuven, Belgium, April 18\u201321, 2006, pp. 73\u201385. ACM (2006)","DOI":"10.1145\/1217935.1217943"},{"key":"302_CR13","doi-asserted-by":"crossref","unstructured":"Bloem, R., Jacobs, S., Khalimov, A.: Parameterized synthesis case study: AMBA AHB. In: Proceedings 3rd Workshop on Synthesis, SYNT 2014, Volume 157 of EPTCS (2014)","DOI":"10.4204\/EPTCS.157.9"},{"issue":"1","key":"302_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2200\/S00658ED1V01Y201508DCT013","volume":"6","author":"R Bloem","year":"2015","unstructured":"Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability of parameterized verification. Synth Lect. Distrib. Comput. Theory 6(1), 1\u2013170 (2015)","journal-title":"Synth Lect. Distrib. Comput. Theory"},{"key":"302_CR15","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1016\/0890-5401(89)90026-6","volume":"81","author":"MC Browne","year":"1989","unstructured":"Browne, M.C., Clarke, E.M., Grumberg, O.: Reasoning about networks with many identical finite state processes. Inf. Comput. 81, 13\u201331 (1989)","journal-title":"Inf. Comput."},{"key":"302_CR16","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Talupur, M., Touili, T., Veith, H.: Verification by network decomposition. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004\u2014Concurrency Theory, 15th International Conference, London, UK, August 31\u2013September 3, 2004, Proceedings, Volume 3170 of Lecture Notes in Computer Science, pp. 276\u2013291. Springer (2004)","DOI":"10.1007\/978-3-540-28644-8_18"},{"key":"302_CR17","volume-title":"Graph Structure and Monadic Second-Order Logic\u2014A Language-Theoretic Approach, Volume 138 of Encyclopedia of Mathematics and its Applications","author":"B Courcelle","year":"2012","unstructured":"Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-Order Logic\u2014A Language-Theoretic Approach, Volume 138 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge (2012)"},{"issue":"2","key":"302_CR18","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/s002249910009","volume":"33","author":"B Courcelle","year":"2000","unstructured":"Courcelle, B., Makowsky, J.A., Rotics, U.: Linear time solvable optimization problems on graphs of bounded clique-width. Theory Comput. Syst. 33(2), 125\u2013150 (2000)","journal-title":"Theory Comput. Syst."},{"issue":"1","key":"302_CR19","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/S0166-218X(99)00184-5","volume":"101","author":"B Courcelle","year":"2000","unstructured":"Courcelle, B., Olariu, S.: Upper bounds to the clique width of graphs. Discrete Appl. Math. 101(1), 77\u2013114 (2000)","journal-title":"Discrete Appl. Math."},{"key":"302_CR20","doi-asserted-by":"crossref","unstructured":"Delzanno, G., Raskin, J.-F., Van Begin, L.: Towards the automated verification of multithreaded java programs. In: Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS \u201902. Springer (2002)","DOI":"10.1007\/3-540-46002-0_13"},{"key":"302_CR21","doi-asserted-by":"crossref","unstructured":"Delzanno, G., Sangnier, A., Traverso, R.: Parameterized verification of broadcast networks of register automata. In: Proceedings of the 7th International Workshop on Reachability Problems (RP\u201913), Volume 8169 of Lecture Notes in Computer Science. Springer (2013)","DOI":"10.1007\/978-3-642-41036-9_11"},{"key":"302_CR22","doi-asserted-by":"publisher","unstructured":"Delzanno, G., Traverso, R.: Decidability and complexity results for verification of asynchronous broadcast networks. In: Dediu, A-H., Mart\u00edn-Vide, C., Truthe, B. (eds.) Language and Automata Theory and Applications: 7th International Conference, LATA 2013, Bilbao, Spain, 2-5 April 2013, Proceedings, pp. 239\u2013249, Springer, Berlin, Heidelberg (2013). doi: 10.1007\/978-3-642-37064-9_22","DOI":"10.1007\/978-3-642-37064-9_22"},{"key":"302_CR23","volume-title":"Finite Model Theory","author":"H-D Ebbinghaus","year":"2005","unstructured":"Ebbinghaus, H.-D., Flum, J.: Finite Model Theory. Springer, Berlin (2005)"},{"key":"302_CR24","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: CADE. Springer (2000)","DOI":"10.1007\/10721959_19"},{"key":"302_CR25","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Kahlon, V.: Exact and efficient verification of parameterized cache coherence protocols. In: Geist, D., Tronci, E. (eds.) Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L\u2019Aquila, Italy, October 21\u201324, 2003, Proceedings, Volume 2860 of Lecture Notes in Computer Science, pp. 247\u2013262. Springer (2003)","DOI":"10.1007\/978-3-540-39724-3_22"},{"key":"302_CR26","doi-asserted-by":"crossref","unstructured":"Emerson, E. A., Kahlon, V.: Parameterized model checking of ring-based message passing systems. In: Marcinkowski, J., Tarlecki, A. (eds.) Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20\u201324, 2004, Proceedings, Volume 3210 of Lecture Notes in Computer Science, pp. 325\u2013339. Springer (2004)","DOI":"10.1007\/978-3-540-30124-0_26"},{"key":"302_CR27","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Namjoshi, K.S.: On model checking for non-deterministic infinite-state systems. In: Thirteenth Annual IEEE Symposium on Logic in Computer Science, Indianapolis, Indiana, USA, June 21\u201324, 1998, pp. 70\u201380. IEEE Computer Society (1998)","DOI":"10.1109\/LICS.1998.705644"},{"issue":"4","key":"302_CR28","doi-asserted-by":"crossref","first-page":"527","DOI":"10.1142\/S0129054103001881","volume":"14","author":"EA Emerson","year":"2003","unstructured":"Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. Int. J. Found. Comput. Sci. 14(4), 527\u2013549 (2003)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"302_CR29","doi-asserted-by":"publisher","unstructured":"Esparza, J.: Decidability and complexity of petri net problems\u2014an introduction. In: Reisig, W., Rozenberg, G. (eds.) Lectures on Petri Nets I: Basic Models: Advances in Petri Nets, pp. 374\u2013428, Springer, Berlin, Heidelberg. doi: 10.1007\/3-540-65306-6_20","DOI":"10.1007\/3-540-65306-6_20"},{"key":"302_CR30","unstructured":"Esparza, J.: Keeping a crowd safe: on the complexity of parameterized verification (invited talk). In: Mayr, E.W., Portier, N. (eds.) 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014), STACS 2014, March 5\u20138, 2014, Lyon, France, Volume 25 of LIPIcs, pp. 1\u201310. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2014)"},{"key":"302_CR31","doi-asserted-by":"crossref","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2\u20135, 1999, pp. 352\u2013359. IEEE Computer Society (1999)","DOI":"10.1109\/LICS.1999.782630"},{"key":"302_CR32","unstructured":"Esparza, J., Ganty, P., Leroux, J., Majumdar, R.: Verification of population protocols. In: 26th International Conference on Concurrency Theory, CONCUR 2015, Volume 42 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)"},{"key":"302_CR33","doi-asserted-by":"crossref","unstructured":"Fischer, E., Makowsky, J.A.: The Specker-Blatter theorem revisited. In: Computing and Combinatorics, 9th Annual International Conference, COCOON 2003, Proceedings (2003)","DOI":"10.1007\/3-540-45071-8_11"},{"key":"302_CR34","doi-asserted-by":"publisher","unstructured":"Fischer, E., Makowsky, J.A.: Linear recurrence relations for graph polynomials. In: In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science: Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, pp. 266\u2013279, Springer, Berlin, Heidelberg (2008). doi: 10.1007\/978-3-540-78127-1_15","DOI":"10.1007\/978-3-540-78127-1_15"},{"key":"302_CR35","volume-title":"Parameterized Complexity Theory (Texts in Theoretical Computer Science. An EATCS Series)","author":"J Flum","year":"2006","unstructured":"Flum, J., Grohe, M.: Parameterized Complexity Theory (Texts in Theoretical Computer Science. An EATCS Series). Springer, Berlin (2006)"},{"issue":"3","key":"302_CR36","doi-asserted-by":"crossref","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"SM German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675\u2013735 (1992)","journal-title":"J. ACM"},{"issue":"2","key":"302_CR37","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/0020-0190(96)00095-6","volume":"59","author":"I Glaister","year":"1996","unstructured":"Glaister, I., Shallit, J.: A lower bound technique for the size of nondeterministic finite automata. Inf. Process. Lett. 59(2), 75\u201377 (1996)","journal-title":"Inf. Process. Lett."},{"key":"302_CR38","doi-asserted-by":"crossref","unstructured":"Gmeiner, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Tutorial on parameterized model checking of fault-tolerant distributed algorithms. In: Formal Methods for Executable Software Models\u201414th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2014, Bertinoro, Italy, June 16\u201320, 2014, Advanced Lectures, pp. 122\u2013171 (2014)","DOI":"10.1007\/978-3-319-07317-0_4"},{"key":"302_CR39","unstructured":"Graham, R.L., Knuth, D.E., Patashnik, O.: Concrete Mathematics: A Foundation for Computer Science, 2nd edn. Addison-Wesley, Reading (1994)"},{"key":"302_CR40","doi-asserted-by":"crossref","unstructured":"Jacobs, S., Bloem, R.: Parameterized synthesis. Log. Methods Comput. Sci. 10(1), 362\u2013376 (2014)","DOI":"10.2168\/LMCS-10(1:12)2014"},{"key":"302_CR41","doi-asserted-by":"crossref","unstructured":"John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Counter attack on byzantine generals: parameterized model checking of fault-tolerant distributed algorithms. CoRR, abs\/1210.3846 (2012)","DOI":"10.1109\/FMCAD.2013.6679411"},{"key":"302_CR42","doi-asserted-by":"crossref","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: Touili, T., Cook, B., Jackson, P.B. (eds.) Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15\u201319, 2010. Proceedings, Volume 6174 of Lecture Notes in Computer Science, pp. 645\u2013659. Springer (2010)","DOI":"10.1007\/978-3-642-14295-6_55"},{"key":"302_CR43","doi-asserted-by":"crossref","unstructured":"Khalimov, A., Jacobs, S., Bloem, R.: PARTY parameterized synthesis of token rings. In: Computer Aided Verification\u201425th International Conference, CAV 2013, Proceedings, Volume 8044 of Lecture Notes in Computer Science. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_66"},{"key":"302_CR44","doi-asserted-by":"crossref","unstructured":"Libkin, L.: Elements of Finite Model Theory. In: Brauer, W., Rozenburg, G., Salomaa, A. (eds.) Texts in Theoretical Computer Science. An EATCS Series. Springer Berlin, Heidelberg (2004)","DOI":"10.1007\/978-3-662-07003-1"},{"key":"302_CR45","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/j.apal.2003.11.002","volume":"126","author":"JA Makowsky","year":"2004","unstructured":"Makowsky, J.A.: Algorithmic uses of the Feferman\u2013Vaught theorem. Ann. Pure Appl. Log. 126, 159\u2013213 (2004)","journal-title":"Ann. Pure Appl. Log."},{"key":"302_CR46","volume-title":"Computation: Finite and Infinite Machines","author":"ML Minsky","year":"1967","unstructured":"Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall, Inc., Englewood Cliffs (1967)"},{"key":"302_CR47","unstructured":"Rubin, S.: Parameterised verification of autonomous mobile-agents in static but unknown environments. In: Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015, pp. 199\u2013208 (2015)"},{"key":"302_CR48","doi-asserted-by":"crossref","unstructured":"Schmitz, S., Schnoebelen, P.: The power of well-structured systems. In: D\u2019Argenio, P.R., Melgratti, H.C. (eds.) CONCUR 2013\u2014Concurrency Theory\u201424th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, Volume 8052 of Lecture Notes in Computer Science, pp. 5\u201324. Springer (2013)","DOI":"10.1007\/978-3-642-40184-8_2"},{"issue":"1","key":"302_CR49","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/S1571-0661(05)82504-6","volume":"39","author":"S Shamir","year":"2003","unstructured":"Shamir, S., Kupferman, O., Shamir, E.: Branching-depth hierarchies. Electron. Notes Theor. Comput. Sci. 39(1), 65\u201378 (2003)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"3","key":"302_CR50","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM (JACM) 32(3), 733\u2013749 (1985)","journal-title":"J. ACM (JACM)"},{"key":"302_CR51","doi-asserted-by":"crossref","unstructured":"Spalazzi, L., Spegni, F.: Parameterized model-checking of timed systems with conjunctive guards. In: Verified Software: Theories, Tools and Experiments\u20146th International Conference, VSTTE 2014, Volume 8471 of Lecture Notes in Computer Science. Springer (2014)","DOI":"10.1007\/978-3-319-12154-3_15"},{"issue":"4","key":"302_CR52","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1016\/0020-0190(88)90211-6","volume":"28","author":"I Suzuki","year":"1988","unstructured":"Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 28(4), 213\u2013214 (1988)","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"302_CR53","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M Vardi","year":"1986","unstructured":"Vardi, M., Wolper, P.: Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Sci. 32(2), 183\u2013221 (1986)","journal-title":"J. Comput. Syst. Sci."}],"container-title":["Distributed Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00446-017-0302-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00446-017-0302-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00446-017-0302-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,25]],"date-time":"2019-09-25T13:28:53Z","timestamp":1569418133000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00446-017-0302-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,6,6]]},"references-count":53,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["302"],"URL":"https:\/\/doi.org\/10.1007\/s00446-017-0302-6","relation":{},"ISSN":["0178-2770","1432-0452"],"issn-type":[{"value":"0178-2770","type":"print"},{"value":"1432-0452","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,6,6]]}}}