×

zbMATH — the first resource for mathematics

Bounded synthesis for Petri games. (English) Zbl 1443.68110
Meyer, Roland (ed.) et al., Correct system design. Symposium in honor of Ernst-Rüdiger Olderog on the occasion of his 60th birthday, Oldenburg, Germany, September 8–9, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9360, 223-237 (2015).
Summary: Petri games, introduced in recent joint work with Ernst- Rüdiger Olderog, are an extension of Petri nets for the causality-based synthesis of distributed systems. In a Petri game, each token is a player in a multiplayer game, played between the “environment” and “system” teams. In this paper, we propose a new technique for finding winning strategies for the system players based on the bounded synthesis approach. In bounded synthesis, we limit the size of the strategy. By incrementally increasing the bound, we can focus the search towards small solutions while still eventually finding every finite winning strategy.
For the entire collection see [Zbl 1320.68024].

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
91A80 Applications of game theory
Software:
DepQBF
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society 138 (1969) · Zbl 0182.02302
[2] Church, A.: Applications of recursive arithmetic to the problem of circuit synthesis. In: Summaries of the Summer Institute of Symbolic Logic, vol. 1, pp. 3–50. Cornell Univ., Ithaca (1957)
[3] Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.Y.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 436. Springer, Heidelberg (2001) · Zbl 0991.68637 · doi:10.1007/3-540-44585-4_43
[4] Finkbeiner, B., Gieseking, M., Olderog, E.-R.: ADAM: causality-based synthesis of distributed systems. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 433–439. Springer, Heidelberg (2015) · Zbl 06845672 · doi:10.1007/978-3-319-21690-4_25
[5] Finkbeiner, B., Olderog, E.: Petri games: synthesis of distributed systems with causal memory. In: Peron, A., Piazza, C. (eds.) Proc. Fifth Intern. Symp. on Games, Automata, Logics and Formal Verification (GandALF). EPTCS, vol. 161, pp. 217–230 (2014). http://dx.doi.org/10.4204/EPTCS.161.19 · doi:10.4204/EPTCS.161.19
[6] Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: Proc. LICS, pp. 321–330. IEEE Computer Society Press (2005) · Zbl 1170.68539 · doi:10.1109/LICS.2005.53
[7] Finkbeiner, B., Schewe, S.: Bounded synthesis. International Journal on Software Tools for Technology Transfer 15(5–6), 519–539 (2013). http://dx.doi.org/10.1007/s10009-012-0228-z · Zbl 1141.68491 · doi:10.1007/s10009-012-0228-z
[8] Gastin, P., Lerman, B., Zeitoun, M.: Distributed games with causal memory are decidable for series-parallel systems. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 275–286. Springer, Heidelberg (2004) · Zbl 1117.68448 · doi:10.1007/978-3-540-30538-5_23
[9] Genest, B., Gimbert, H., Muscholl, A., Walukiewicz, I.: Asynchronous games over tree architectures. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 275–286. Springer, Heidelberg (2013) · Zbl 1334.68150 · doi:10.1007/978-3-642-39212-2_26
[10] Green, C.: Application of theorem proving to problem solving. In: Proceedings of the 1st International Joint Conference on Artificial Intelligence. IJCAI 1969, pp. 219–239. Morgan Kaufmann Publishers Inc., San Francisco (1969). http://dl.acm.org/citation.cfm?id=1624562.1624585
[11] Heljanko, K.: Bounded reachability checking with process semantics. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 218–232. Springer, Heidelberg (2001) · Zbl 1006.68081 · doi:10.1007/3-540-44685-0_15
[12] Junttila, T.A., Niemelä, I.: Towards an efficient tableau method for boolean circuit satisfiability checking. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 553–567. Springer, Heidelberg (2000) · Zbl 0983.68176 · doi:10.1007/3-540-44957-4_37
[13] Kupferman, O., Vardi, M.Y.: Synthesizing distributed systems. In: Proc. LICS, pp. 389–398. IEEE Computer Society Press (2001)
[14] Lonsing, F., Biere, A.: DepQBF: A dependency-aware QBF solver. JSAT 7(2–3), 71–76 (2010)
[15] Madhusudan, P., Thiagarajan, P.S., Yang, S.: The MSO theory of connectedly communicating processes. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 201–212. Springer, Heidelberg (2005) · Zbl 1172.68556 · doi:10.1007/11590156_16
[16] Madhusudan, P., Thiagarajan, P.S.: Distributed controller synthesis for local specifications. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, p. 396. Springer, Heidelberg (2001) · Zbl 0986.68079 · doi:10.1007/3-540-48224-5_33
[17] Mangassarian, H.: QBF-based formal verification: Experience and perspectives. JSAT 133–191 · Zbl 1172.68538
[18] Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Proc. FOCS 1990, pp. 746–757 (1990) · doi:10.1109/FSCS.1990.89597
[19] Rabin, M.O.: Automata on Infinite Objects and Church’s Problem, Regional Conference Series in Mathematics, vol. 13. Amer. Math. Soc. (1972) · Zbl 0315.02037 · doi:10.1090/cbms/013
[20] Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 474–488. Springer, Heidelberg (2007) · Zbl 1141.68491 · doi:10.1007/978-3-540-75596-8_33
[21] Zielonka, W.: Asynchronous automata. In: Rozenberg, G., Diekert, V. (eds.) Book of Traces, pp. 205–248. World Scientific (1995) · doi:10.1142/9789814261456_0007
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.