Abstract
In the classical synthesis problem, we are given a specification ψ over sets of input and output signals, and we synthesize a finite-state transducer that realizes ψ: with every sequence of input signals, the transducer associates a sequence of output signals so that the generated computation satisfies ψ. In recent years, researchers consider extensions of the classical Boolean setting to a multi-valued one. We study a multi-valued setting in which the truth values of the input and output signals are taken from a finite lattice, and so is the satisfaction value of specifications. We consider specifications in latticed linear temporal logic (LLTL). In LLTL, conjunctions and disjunctions correspond to the meet and join operators of the lattice, respectively, and the satisfaction values of formulas are taken from the lattice too. The lattice setting arises in practice, for example in specifications involving priorities or in systems with inconsistent viewpoints. We solve the LLTL synthesis problem, where the goal is to synthesize a transducer that realizes the given specification in a desired satisfaction value. For the classical synthesis problem, researchers have studied a setting with incomplete information, where the truth values of some of the input signals are hidden and the transducer should nevertheless realize ψ. For the multi-valued setting, we introduce and study a new type of incomplete information, where the truth values of some of the input signals may be noisy, and the transducer should still realize ψ in the desired satisfaction value. We study the problem of noisy LLTL synthesis, as well as the theoretical aspects of the setting, like the amount of noise a transducer may tolerate, or the effect of perturbing input signals on the satisfaction value of a specification. We prove that the noisy-synthesis problem for LLTL is 2EXPTIME-complete, as is traditional LTL synthesis.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Notes
In Pnueli and Rosner (1989a) and other early works the games are formulated by means of tree automata.
State-of-the-art algorithms for solving parity games achieve a better complexity (Jurdzinski et al. 2008; Schewe 2007). The bound, however, remains polynomial in the size of the game and exponential in its index. Since the challenge of solving parity games is orthogonal to our contribution here, we keep this component of our contribution simple.
It may be the case that some of the nodes coincide, and this is not a proper N5. However, these cases are easy to handle.
References
Almagor S, Boker U, Kupferman O (2013) ForMalizing and reasoning about quality. In: Proceedings of the 40th int. Colloq. on automata, languages, and programming, volume 7966 of lecture notes in computer science, pp 15–27. Springer
Almagor S, Boker U, Kupferman O (2016) Formally reasoning about quality. J ACM 63(3):24
Almagor S, Kuperberg D, Kupferman O (2015) The sensing cost of monitoring and synthesis. In: 35th IARCS annual conference on foundation of software technology and theoretical computer science, FSTTCS 2015, december 16-18, 2015, Bangalore, India, pp 380–393
Alur R, Kanade A, Weiss G (2008) Ranking automata and games for prioritized requirements. In: Proc. 20th int. Conf. on computer aided verification, volume 5123 of lecture notes in computer science, pp 240–253. Springer
Baier C, Klein J, Klüppelholz S, Märcker S (2014) Computing conditional probabilities in markovian models efficiently. In: 20Th TACAS, pp 515–530
Bloem R, Chatterjee K, Henzinger T, Jobstmann B (2009) Better quality in synthesis through quantitative objectives. In: Proc. 21st int. Conf. on computer aided verification, volume 5643 of lecture notes in computer science, pp 140–156. Springer
Cerný P, Henzinger T (2011) From boolean to quantitative synthesis. In: EMSOFT, pp 149–154
Chatterjee K, Doyen L, Henzinger T (2008) Quantative languages. In: Proceedings of the 17th annual conference of the european association for computer science logic, pp 385–400
Chatterjee K, Doyen L, Henzinger TA, Raskin J-F (2006) Algorithms for omega-regular games with imperfect information. In: Proceedings of the 15th annual conference of the european association for computer science logic, volume 4207 of lecture notes in computer science, pp 287–302
Chatterjee K, Jurdzinski M, Henzinger TA (2004) Quantitative stochastic parity games. In: Proceedings of the fifteenth annual ACM-SIAM symposium on discrete algorithms, SODA 2004, New Orleans, Louisiana, USA, January 11-14, 2004, pp 121–130
Chatterjee K, Majumdar R (2011) Minimum attention controller synthesis for omega-regular objectives FORMATS, pp 145–159
Chatterjee K, Majumdar R, Henzinger TA (2008) Controller synthesis with budget constraints. In: Proceedings of the 11th international workshop on hybrid systems: computation and control, volume 4981 of lecture notes in computer science, pp 72–86. Springer
Chechik M, Devereux B, Gurfinkel A (2001) Model-checking infinite state-space systems with fine-grained abstractions using SPIN. In: Proceedings of the 8th international SPIN workshop on model checking software, volume 2057 of lecture notes in computer science, pp 16–36. Springer
Church A (1963) Logic, arithmetics, and automata. In: Proceedings of the international congress of mathematicians, 1962, pp 23–35. Institut Mittag-Leffler
Emerson E, Jutla C (1991) Tree automata, μ-calculus and determinacy. In: Proceedings of the 32nd IEEE symposium on foundations of computer science, pp 368–377
Faella M, Legay A, Stoelinga M (2008) Model checking quantitative linear time logic. Electr Notes Theor Comput Sci 220(3):61–77
Filiot E, Jin N, Raskin J-F (2009) An antichain algorithm for LTL realizability. In: Proceedings of the 21st international conference on computer aided verification, vol 5643, pp 263–277
Huth M, Pradhan S (2004) Consistent partial model checking. Electr Notes Theor Comput Sci 73:45–85
Jurdzinski M, Paterson M, Zwick U (2008) A deterministic subexponential algorithm for solving parity games. SIAM J Comput 38(4):1519–1532
Kumar R, Shayman M (1995) Supervisory control of nondeterministic systems under partial observation and decentralization. SIAM Journal of Control and Optimization
Kupferman O, Lustig Y (2007) Lattice automata. In: Proceedings of the 8th international conference on verification, model checking, and abstract interpretation, volume 4349 of lecture notes in computer science, pp 199–213. Springer
Kupferman O, Lustig Y (2010) Latticed simulation relations and games. Int J Found Comput Sci 21(2):167–189
Kupferman O, Vardi M (1999) Church’s problem revisited. Bull Symb Log 5 (2):245–263
Kupferman O, Vardi M (2000) Synthesis with incomplete information. In: Advances in temporal logic, pp 109–127. Kluwer Academic Publishers
Kupferman O, Vardi M (2005) Safraless decision procedures. In: Proceedings of the 46th IEEE symposium on foundations of computer science, pp 531–540
Kwiatkowska M (2007) Quantitative verification: models techniques and tools. In: ESEC/SIGSOFT FSE, pp 449–458
Majumdar R, Render E, Tabuada P (2011) Robust discrete synthesis against unspecified disturbances. In: Proceedings of the 14th ACM international conference on hybrid systems: computation and control, HSCC 2011, Chicago, IL, USA, April 12-14, 2011, pp 211–220
Martin D (1975) Borel determinacy. Ann Math 65:363–371
Miyano S, Hayashi T (1984) Alternating finite automata on ω-words. Theor Comput Sci 32:321–330
Piterman N (2006) From nondeterministic bu̇chi and Streett automata to deterministic parity automata. In: Proceedings of the 21st IEEE symposium on logic in computer science, pp 255–264. IEEE press
Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Proceedings of the 16th ACM symposium on principles of programming languages, pp 179–190
Pnueli A, Rosner R (1989) On the synthesis of an asynchronous reactive module. In: Proceedings of the 16th int. Colloq. on automata, languages, and programming, volume 372 of lecture notes in computer science, pp 652–671. Springer
Reif J (1984) The complexity of two-player games of incomplete information. J Comput Syst Sci 29:274–301
Safra S (1992) Exponential determinization for ω-automata with strong-fairness acceptance condition. In: Proceedings of the 24th ACM symposium on theory of computing
Schewe S (2007) Solving parity games in big steps. In: Proceedings of the 27th conference on foundations of software technology and theoretical computer science, pp 449–460
Topcu U, Ozay N, Liu J, Murray RM (2012) On synthesizing robust discrete controllers under modeling uncertainty. In: Hybrid systems: computation and control (part of CPS week 2012), HSCC’12, Beijing, China, April 17-19, 2012, pp 85–94
Vardi M (2008) From verification to synthesis. In: Proceedings of the 2nd international conference on verified software: theories, tools, experiments, volume 5295 of lecture notes in computer science, page 2. Springer
Vardi M, Wolper P (1994) Reasoning about infinite computations. Inf Comput 115(1):1–37
Velner Y, Rabinovich A (2011) Church synthesis problem for noisy input. In: Proceedings of the 14th international conference on foundations of software science and computation structures, pp 275–289
Author information
Authors and Affiliations
Corresponding author
Additional information
A preliminary version appears in “Latticed-LTL synthesis in the presence of noisy inputs.” Foundations of Software Science and Computation Structures, LNCS 8421, Springer, 2014. This research has received funding from the European Research Council under the EU’s 7-th Framework Programme (FP7/2007-2013) / ERC grant agreement no 278410.
Rights and permissions
About this article
Cite this article
Almagor, S., Kupferman, O. Latticed-LTL synthesis in the presence of noisy inputs. Discrete Event Dyn Syst 27, 547–572 (2017). https://doi.org/10.1007/s10626-017-0242-0
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10626-017-0242-0