Adding Data Registers to Parameterized Networks with Broadcast

• Autorzy: Delzanno, G. , Sangnier, A. , Traverso, R.
• Języki publikacji: EN

Abstrakty

EN

We study parameterized verification problems for networks of interacting register automata. The network is represented through a graph, and processes may exchange broadcast messages containing data with their neighbours. Upon reception a process can either ignore a sent value, test for equality with a value stored in a register, or simply store the value in a register. We consider safety properties expressed in terms of reachability, from arbitrarily large initial configurations, of a configuration exposing some given control states and patterns. We investigate, in this context, the impact on decidability and complexity of the number of local registers, the number of values carried by a single message, and dynamic reconfigurations of the underlying network.

Słowa kluczowe

EN

graph theory; machine theory; problem solving; computational complexity; register

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2016
• Tom: Vol. 143, nr 3/4
• Strony: 287--316
• Opis fizyczny: Bibliogr. 28 poz., rys., tab.

Twórcy

autor

Delzanno, G.

• DIBRIS, University of Genova, Italy,

autor

Sangnier, A.

• LIAFA, Univ Paris Diderot, Paris, Cité Sorbonne, CNRS, France ,

autor

Traverso, R.

• FBK, Trento, Italy,

Bibliografia

• [1] Konnov I, Veith H, Widder J. Who is afraid of Model Checking Distributed Algorithms?; 2012. Unpublished contribution to: CAV Workshop (EC)2. Available from: http://forsyte.at/wp-content/uploads/2012/07/ec2-konnov.pdf.
• [2] German SM, Sistla AP. Reasoning about Systems with Many Processes. J ACM. 1992;39(3):675–735. doi:10.1145/146637.146681.
• [3] Emerson EA, Namjoshi KS. On Model Checking for Non-Deterministic Infinite-State Systems. In: Thirteenth Annual IEEE Symposium on Logic in Computer Science, Indianapolis, Indiana, USA, June 21-24, 1998; 1998. p. 70–80. doi:10.1109/LICS.1998.705644.
• [4] 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-5, 1999; 1999. p. 352–359. doi:10.1109/LICS.1999.782630.
• [5] Abdulla PA, Cerans K, Jonsson B, Tsay Y. General Decidability Theorems for Infinite-State Systems. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996; 1996. p. 313–321. doi:10.1109/LICS.1996.561359.
• [6] Finkel A, Schnoebelen P. Well-structured transition systems everywhere! Theor Comput Sci. 2001;256(1-2):63–92. doi:10.1016/S0304-3975(00)00102-X.
• [7] Delzanno G. Constraint-Based Verification of Parameterized Cache Coherence Protocols. Formal Methods in System Design. 2003;23(3):257–301. doi:10.1023/A:1026276129010.
• [8] Esparza J, Ganty P, Majumdar R. Parameterized Verification of Asynchronous Shared-Memory Systems. In: Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings; 2013. p. 124–140. doi:10.1007/978-3-642-39799-8 8.
• [9] Esparza J. Keeping a Crowd Safe: On the Complexity of Parameterized Verification (Invited Talk). In: 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014), STACS 2014,March 5-8, 2014, Lyon, France; 2014. p. 1–10. doi:10.4230/LIPIcs.STACS.2014.1.
• [10] Aminof B, Jacobs S, Khalimov A, Rubin S. Parameterized Model Checking of Token-Passing Systems. In: Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings; 2014. p. 262–281. doi:10.1007/978-3-642-54013-4 15.
• [11] Clarke EM, Talupur M, Touili T, Veith H. Verification by Network Decomposition. In: CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings; 2004. p. 276–291. doi:10.1007/978-3-540-28644-8 18.
• [12] Bollig B, Gastin P, Schubert J. Parameterized Verification of Communicating Automata under Context Bounds. In: Reachability Problems - 8th International Workshop, RP 2014, Oxford, UK, September 22-24, 2014. Proceedings; 2014. p. 45–57. doi:10.1007/978-3-319-11439-2 4.
• [13] Delzanno G, Rosa-Velardo F. On the coverability and reachability languages of monotonic extensions of Petri nets. Theor Comput Sci. 2013;467:12–29. doi:10.1016/j.tcs.2012.09.021.
• [14] Delzanno G, Sangnier A, Zavattaro G. Parameterized Verification of Ad Hoc Networks. In: CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings; 2010. p. 313–327. doi:10.1007/978-3-642-15375-4 22.
• [15] Delzanno G, Sangnier A, Zavattaro G. On the Power of Cliques in the Parameterized Verification of Ad Hoc Networks. In: Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings; 2011. p. 441–455. doi:10.1007/978-3-642-19805-2 30.
• [16] Delzanno G, Sangnier A, Traverso R, Zavattaro G. On the Complexity of Parameterized Reachability in Reconfigurable Broadcast Networks. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012, December 15-17, 2012, Hyderabad, India; 2012. p. 289–300. doi:10.4230/LIPIcs.FSTTCS.2012.289.
• [17] Alur R, Dill DL. A Theory of Timed Automata. Theor Comput Sci. 1994;126(2):183–235. doi:10.1016/0304-3975(94)90010-8.
• [18] Abdulla PA, Delzanno G, Rezine O, Sangnier A, Traverso R. On the Verification of Timed Ad Hoc Networks. In: Formal Modeling and Analysis of Timed Systems - 9th International Conference, FORMATS 2011, Aalborg, Denmark, September 21-23, 2011. Proceedings; 2011. p. 256–270. doi:10.1007/978-3-642-24310-3 18.
• [19] Bertrand N, Fournier P, Sangnier A. Playing with Probabilities in Reconfigurable Broadcast Networks. In: Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings; 2014. p. 134–148. doi:10.1007/978-3-642-54830-7 9.
• [20] Kaminski M, Francez N. Finite-Memory Automata. Theor Comput Sci. 1994;134(2):329–363. doi:10.1016/0304-3975(94)90242-9.
• [21] Abdulla PA, Jonsson B. Ensuring completeness of symbolic verification methods for infinite-state systems. Theor Comput Sci. 2001;256(1-2):145–167. doi:10.1016/S0304-3975(00)00105-5.
• [22] Schnoebelen P. Revisiting Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets. In: Mathematical Foundations of Computer Science 2010, 35th International Symposium, MFCS 2010, Brno, Czech Republic, August 23-27, 2010. Proceedings; 2010. p. 616–628. doi:10.1007/978-3-642-15155-2 54.
• [23] Delzanno G, Sangnier A, Traverso R. Parameterized Verification of Broadcast Networks of Register Automata. In: Reachability Problems - 7th International Workshop, RP 2013, Uppsala, Sweden, September 24-26, 2013 Proceedings; 2013. p. 109–121. doi:10.1007/978-3-642-41036-9 11.
• [24] Schmitz S, Schnoebelen P. The Power of Well-Structured Systems. In: CONCUR 2013 – Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings; 2013. p. 5–24. doi:10.1007/978-3-642-40184-8 2.
• [25] Minsky M. Computation, Finite and Infinite Machines. Prentice Hall; 1967.
• [26] Cheng A, Esparza J, Palsberg J. Complexity Results for 1-Safe Nets. Theor Comput Sci. 1995;147(1&2): 117–136. doi:10.1016/0304-3975(94)00231-7.
• [27] Lazic R, Newcomb T, Ouaknine J, Roscoe AW, Worrell J. Nets with Tokens which Carry Data. Fundamenta Informaticae 2008;88(3):251–274. Available from: http://content.iospress.com/articles/fundamenta-informaticae/fi88-3-03.
• [28] Delzanno G, Sangnier A, Traverso R. Parameterized Verification of Broadcast Networks of Register Automata (Technical Report). TR-13-03, DIBRIS, University of Genova; 2013. Available at the URL http://verify.disi.unige.it/publications/.

Identyfikatory

DOI

10.3233/FI-2016-1315