×

Compositional construction of most general controllers. (English) Zbl 1329.68186

Authors’ abstract: Given a system \(\mathfrak{A}\) and an objective \(\varPhi\), the task of controller synthesis is to design a decision making policy that ensures \(\varPhi\) to be satisfied. This article deals with transition system-like system models and controllers that base their decisions on the observables of the actions performed so far. We present a framework for the compositional construction of controllers for conjunctive sequences of linear-time objectives in an online manner. For this approach, it is crucial that the controllers enforce the objectives in a most general manner, being as permissive as possible. We then present game-based algorithms for the construction of such most general controllers for invariance, reachability and \(\omega\)-regular objectives.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B44 Temporal logic
68Q60 Specification and verification (program logics, model checking, etc.)
93B50 Synthesis problems

Software:

Reo
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. In: 16th Colloquium on Automata, Languages and Programming (ICALP’89), LNCS, vol. 372, pp. 1-17. Springer (1989) · Zbl 1232.91007
[2] Arbab, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comput. Sci. 14(3), 329-366 (2004) · Zbl 1085.68552
[3] Asarin, E., Bournez, O., Dang, T., Maler, O., Pnueli, A.: Effective synthesis of switching controllers for linear systems. IEEE Spec. Issue Hybrid Syst. 88, 1011-1025 (2000)
[4] Asarin, E., Maler, O., Pnueli, A.: Symbolic controller synthesis for discrete and timed systems. In: Hybrid Systems II, LNCS, vol. 999, pp. 1-20. Springer (1995) · Zbl 0182.02302
[5] Baier, C., Blechmann, T., Klein, J., Klüppelholz, S.: Formal verification for components and connectors. In: 7th Symposium on Formal Methods for Components and Objects (FMCO’08), LNCS, vol. 5751, pp. 82-101. Springer (2008) · Zbl 1254.68143
[6] Baier, C., Blechmann, T., Klein, J., Klüppelholz, S.: A uniform framework for modeling and verifying components and connectors. In: 11th Conference on Coordination Models and Languages (COORD’09), LNCS, vol. 5521, pp. 247-267. Springer (2009) · Zbl 1254.68143
[7] Baier, C., Klein, J., Klüppelholz, S.: A compositional framework for controller synthesis. In: 22nd Conference on Concurrency Theory (CONCUR’11), LNCS, vol. 6901, pp. 512-527. Springer (2011) · Zbl 1329.68182
[8] Baier, C., Klein, J., Klüppelholz, S.: Modeling and verification of components and connectors. In: 11th International School on Formal Methods for the Design of Computer, Communication and Software Systems (SFM’11), LNCS, vol. 6659, pp. 114-147. Springer (2011) · Zbl 0182.02302
[9] Baier, C., Klein, J., Klüppelholz, S.: Synthesis of Reo connectors for strategies and controllers. Fundam. Inform. 130(1), 1-20 (2014) · Zbl 1286.68067
[10] Baier, C., Sirjani, M., Arbab, F., Rutten, J.J.M.M.: Modeling component connectors in Reo by constraint automata. Sci. Comput. Program. 61(2), 75-113 (2006) · Zbl 1105.68058
[11] Bernet, J., Janin, D., Walukiewicz, I.: Permissive strategies: from parity games to safety games. RAIRO Theor. Inf. Appl. 36(3), 261-275 (2002) · Zbl 1090.91514
[12] Berwanger, D., Chatterjee, K., Wulf, M.D., Doyen, L., Henzinger, T.A.: Strategy construction for parity games with imperfect information. Inf. Comput. 208(10), 1206-1220 (2010) · Zbl 1232.91007
[13] Berwanger, D., Doyen, L.: On the power of imperfect information. In: 28th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’08), Leibniz International Proceedings in Informatics, vol. 2, pp. 73-82. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2008) · Zbl 1248.68233
[14] Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of Reactive(1) designs. J. Comput. Syst. Sci. 78(3), 911-938 (2012) · Zbl 1247.68050
[15] Bouyer, P., Duflot, M., Markey, N., Renault, G.: Measuring permissivity in finite games. In: 20th Conference on Concurrency Theory (CONCUR’09), LNCS, vol. 5710, pp. 196-210. Springer (2009) · Zbl 1254.91033
[16] Bouyer, P., Markey, N., Olschewski, J., Ummels, M.: Measuring permissiveness in parity games: Mean-payoff parity games revisited. In: 9th Symposium on Automated Technology for Verification and Analysis (ATVA’11), LNCS, vol. 6996, pp. 135-149. Springer (2011) · Zbl 1348.68093
[17] Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138, 295-311 (1969) · Zbl 0182.02302
[18] Chatterjee, K., Doyen, L.: The complexity of partial-observation parity games. In: 17th Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR’10), LNCS, vol. 6397, pp. 1-14. Springer (2010) · Zbl 1298.91050
[19] Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Environment assumptions for synthesis. In: 19th Conference on Concurrency Theory (CONCUR’08), LNCS, vol. 5201, pp. 147-161. Springer (2008) · Zbl 1160.68437
[20] Church, A.: Logic, arithmetic, and automata. In: Proceedings of the International Congress of Mathematicians (ICM’62), pp. 23-35. Institut Mittag-Leffler (1963) · Zbl 0116.33604
[21] Dziembowski, S., Jurdzinski, M., Walukiewicz, I.: How much memory is needed to win infinite games? In: 12th Symposium on Logic in Computer Science (LICS’97), pp. 99-110. IEEE Computer Society Press (1997)
[22] Ehlers, R., Finkbeiner, B.: Reactive safety. In: 2nd Symposium on Games, Automata, Logics and Formal Verification (GandALF’11), EPTCS, vol. 54, pp. 178-191 (2011) · Zbl 1457.68163
[23] Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. In: 29th Symposium on Foundations of Computer Science (FOCS’88), pp. 328-337. IEEE Computer Society Press (1988) · Zbl 0937.68074
[24] Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. SIAM J. Comput. 29(1), 132-158 (1999) · Zbl 0937.68074
[25] Filiot, E., Jin, N., Raskin, J.F.: Compositional algorithms for LTL synthesis. In: 8th Symposium on Automated Technology for Verification and Analysis (ATVA’10), LNCS, vol. 6252, pp. 112-127. Springer (2010) · Zbl 1305.68118
[26] Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research, LNCS, vol. 2500. Springer (2002) · Zbl 1011.00037
[27] Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: 6th Conference on Formal Methods in Computer-Aided Design (FMCAD’06), pp. 117-124. IEEE Computer Society Press (2006)
[28] Jobstmann, B., Galler, S.J., Weiglhofer, M., Bloem, R.: Anzu: A tool for property synthesis. In: 19th Conference on Computer Aided Verification (CAV’07), LNCS, vol. 4590, pp. 258-262. Springer (2007)
[29] Klein, J.: Compositional synthesis and most general controllers. Ph.D. thesis, Technische Universität Dresden (2013). http://nbn-resolving.de/urn:nbn:de:bsz:14-qucosa-130654
[30] Kuijper, W., van de Pol, J.: Compositional control synthesis for partially observable systems. In: 20th Conference on Concurrency Theory (CONCUR’09), LNCS, vol. 5710, pp. 431-447. Springer (2009) · Zbl 1254.93075
[31] Kuijper, W., van de Pol, J.: Computing weakest strategies for safety games of imperfect information. In: 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’09), LNCS, vol. 5505, pp. 92-106. Springer (2009) · Zbl 1234.68259
[32] Kupferman, O., Madhusudan, P., Thiagarajan, P.S., Vardi, M.Y.: Open systems in reactive environments: Control and synthesis. In: 11th Conference on Concurrency Theory (CONCUR’00), LNCS, vol. 1877, pp. 92-107 (2000) · Zbl 0999.68124
[33] Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: 18th Conference on Computer Aided Verification (CAV’06), LNCS, vol. 4144, pp. 31-44. Springer (2006) · Zbl 1188.68193
[34] Kupferman, O., Vardi, M.Y.: Synthesis with incomplete informatio. In: 2nd International Conference on Temporal Logic (ICTL’97), pp. 91-106. Kluwer Academic Publishers (1997) · Zbl 1105.68058
[35] Kupferman, O., Vardi, M.Y.: Synthesis of trigger properties. In: 16th Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR’10), LNCS, vol. 6355, pp. 312-331. Springer (2010) · Zbl 1310.68143
[36] Kupferman, O., Weiner, S.: Environment-friendly safety. In: 8th Haifa Verification Conference (HVC’12), LNCS, vol. 7857, pp. 227-242. Springer (2013) · Zbl 0618.93033
[37] Mari, F., Melatti, I., Salvo, I., Tronci, E.: Model-based synthesis of control software from system-level formal specifications. ACM Trans. Softw. Eng. Methodol. 23(1), 6 (2014)
[38] Mohalik, S., Walukiewicz, I.: Distributed games. In: 23rd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’03), LNCS, vol. 2914, pp. 338-351 (2003) · Zbl 1205.68089
[39] Morgenstern, A.: Symbolic controller synthesis for LTL specifications. Ph.D. thesis, Technische Universität Kaiserslautern (2010)
[40] Morgenstern, A., Schneider, K.: Exploiting the temporal logic hierarchy and the non-confluence property for efficient LTL synthesis. In: 1st Symposium on Games, Automata, Logic, and Formal Verification (GandALF’10), Electronic Proceedings in Theoretical Computer Science, vol. 25, pp. 89-102. Elsevier (2010) · Zbl 1456.68099
[41] Neider, D., Rabinovich, R., Zimmermann, M.: Down the borel hierarchy: Solving Muller games via safety games. In: 3rd Symposium on Games, Automata, Logics and Formal Verification (GandALF’12), Electronic Proceedings in Theoretical Computer Science, vol. 96, pp. 169-182. Elsevier (2012) · Zbl 1314.91053
[42] Pinchinat, S., Riedweg, S.: You can always compute maximally permissive controllers under partial observation when they exist. In: 2005 American Control Conference (2005) · Zbl 1177.93059
[43] Pnueli, A.: The temporal logic of programs. In: 18th Symposium on Foundations of Computer Science (FOCS’77), pp. 46-57. IEEE Computer Society Press (1977)
[44] Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: 16th ACM Symposium on Principles of Programming Languages (POPL’89), pp. 179-190. ACM (1989) · Zbl 0686.68015
[45] Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: 31st Symposium on Foundations of Computer Science (FOCS’90), Volume II, pp. 746-757. IEEE Computer Society Press (1990)
[46] Puchala, B.: Asynchronous omega-regular games with partial information. In: 35th Symposium on the Mathematical Foundations of Computer Science (MFCS’10), LNCS, vol. 6281, pp. 592-603. Springer (2010) · Zbl 1287.68111
[47] Rabin, M.O.: Automata on Infinite Objects and Church’s Problem. American Mathematical Society (1972) · Zbl 0315.02037
[48] Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25(1), 206-230 (1987) · Zbl 0618.93033
[49] Raskin, J.F., Chatterjee, K., Doyen, L., Henzinger, T.A.: Algorithms for \[\omega\] ω-regular games with imperfect information. Log. Methods Comput. Sci. 3(3:4), 1-23 (2007) · Zbl 1125.91028
[50] Reif, J.H.: The complexity of two-player games of incomplete information. J. Comput. Syst. Sci. 29(2), 274-301 (1984) · Zbl 0551.90100
[51] Sohail, S., Somenzi, F.: Safety first: a two-stage algorithm for the synthesis of reactive systems. STTT 15(5-6), 433-454 (2013)
[52] Thomas, W.: Languages, automata, and logic. In: Handbook of Formal Languages, vol. III, pp. 389-455. Springer (1997) · Zbl 1247.68050
[53] Vardi, M.Y.: An automata-theoretic approach to fair realizability and synthesis. In: 7th Conference on Computer Aided Verification (CAV’95), LNCS, vol. 939, pp. 267-278. Springer (1995)
[54] Wonham, W.M.: On the control of discrete-event systems. In: Three Decades of Mathematical System Theory, Lecture Notes in Control and Information Sciences, vol. 135, pp. 542-562. Springer (1989) · Zbl 0705.93056
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.