Skip to main content
Erschienen in: Acta Informatica 1-2/2020

09.11.2019 | Original Article

Reactive synthesis with maximum realizability of linear temporal logic specifications

verfasst von: Rayna Dimitrova, Mahsa Ghasemi, Ufuk Topcu

Erschienen in: Acta Informatica | Ausgabe 1-2/2020

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

A challenging problem for autonomous systems is to synthesize a reactive controller that conforms to a set of given correctness properties. Linear temporal logic (LTL) provides a formal language to specify the desired behavioral properties of systems. In applications in which the specifications originate from various aspects of the system design, or consist of a large set of formulas, the overall system specification may be unrealizable. Driven by this fact, we develop an optimization variant of synthesis from LTL formulas, where the goal is to design a controller that satisfies a set of hard specifications and minimally violates a set of soft specifications. To that end, we introduce a value function that, by exploiting the LTL semantics, quantifies the level of violation of properties. Inspired by the idea of bounded synthesis, we fix a bound on the implementation size and search for an implementation that is optimal with respect to the said value function. We propose a novel maximum satisfiability encoding of the search for an optimal implementation (within the given bound on the implementation size). We iteratively increase the bound on the implementation size until a termination criterion, such as a threshold over the value function, is met.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Fußnoten
2
There can be different indices i for which \(e_i = p\) at the same time. While this will be redundant, it does not affect the encoding.
 
Literatur
1.
2.
Zurück zum Zitat Alur, R., Kanade, A., Weiss, G.: Ranking automata and games for prioritized requirements. In: Proceedings of International Conference on Computer-Aided Verification, vol. 5123 of LNCS (2008) Alur, R., Kanade, A., Weiss, G.: Ranking automata and games for prioritized requirements. In: Proceedings of International Conference on Computer-Aided Verification, vol. 5123 of LNCS (2008)
3.
Zurück zum Zitat Baier, C., Katoen, J.: Principles of model checking. MIT press (2008) Baier, C., Katoen, J.: Principles of model checking. MIT press (2008)
4.
Zurück zum Zitat Berg, J., Hyttinen, A., Järvisalo, M.: Applications of MaxSAT in data analysis. In: Pragmatics of SAT (2015) Berg, J., Hyttinen, A., Järvisalo, M.: Applications of MaxSAT in data analysis. In: Pragmatics of SAT (2015)
5.
Zurück zum Zitat Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability, vol. 185. IOS Press, Amsterdam (2009)MATH Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability, vol. 185. IOS Press, Amsterdam (2009)MATH
6.
Zurück zum Zitat Bloem, R., Chatterjee, K., Henzinger, T. A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Proceedings of International Conference on Computer-Aided Verification, vol. 5643 of LNCS, pp. 140–156 (2009)CrossRef Bloem, R., Chatterjee, K., Henzinger, T. A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Proceedings of International Conference on Computer-Aided Verification, vol. 5643 of LNCS, pp. 140–156 (2009)CrossRef
7.
Zurück zum Zitat Cimatti, A., Roveri, M., Schuppan, V., Tchaltsev, A.: Diagnostic information for realizability. In: Proceedings of International Conference on Verification, Model Checking, and Abstract Interpretation, LNCS (2008) Cimatti, A., Roveri, M., Schuppan, V., Tchaltsev, A.: Diagnostic information for realizability. In: Proceedings of International Conference on Verification, Model Checking, and Abstract Interpretation, LNCS (2008)
8.
Zurück zum Zitat Cimatti, A., Roveri, M., Schuppan, V., Tonetta, S.: Boolean abstraction for temporal logic satisfiability. In: Proceedings of International Conference on Computer-Aided Verification, vol. 4590 of LNCS, pp. 532–546 (2007)CrossRef Cimatti, A., Roveri, M., Schuppan, V., Tonetta, S.: Boolean abstraction for temporal logic satisfiability. In: Proceedings of International Conference on Computer-Aided Verification, vol. 4590 of LNCS, pp. 532–546 (2007)CrossRef
9.
Zurück zum Zitat Dimitrova, R., Ghasemi, M., Topcu, U.: Maximum realizability for linear temporal logic specifications. In: Proceedings of Automated Technology for Verification and Analysis, pp. 458–475. Springer (2018) Dimitrova, R., Ghasemi, M., Topcu, U.: Maximum realizability for linear temporal logic specifications. In: Proceedings of Automated Technology for Verification and Analysis, pp. 458–475. Springer (2018)
10.
Zurück zum Zitat Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0—a framework for LTL and \(\omega \)-automata manipulation. In: Proceedings of Automated Technology for Verification and Analysis, vol. 9938 of LNCS (2016)CrossRef Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0—a framework for LTL and \(\omega \)-automata manipulation. In: Proceedings of Automated Technology for Verification and Analysis, vol. 9938 of LNCS (2016)CrossRef
11.
Zurück zum Zitat Ehlers, R., Raman, V.: Low-effort specification debugging and analysis. In: Proceedings of Workshop on Synthesis, vol. 157 of EPTCS, pp. 117–133 (2014)MathSciNetCrossRef Ehlers, R., Raman, V.: Low-effort specification debugging and analysis. In: Proceedings of Workshop on Synthesis, vol. 157 of EPTCS, pp. 117–133 (2014)MathSciNetCrossRef
12.
Zurück zum Zitat Faymonville, P., Finkbeiner, B., Rabe, M. N., Tentrup, L.: Encodings of bounded synthesis. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 10205 of LNCS, pp. 354–370 (2017)CrossRef Faymonville, P., Finkbeiner, B., Rabe, M. N., Tentrup, L.: Encodings of bounded synthesis. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 10205 of LNCS, pp. 354–370 (2017)CrossRef
13.
Zurück zum Zitat Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Softw. Tools Technol. Transf. 15(5–6), 519–539 (2013) CrossRef Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Softw. Tools Technol. Transf. 15(5–6), 519–539 (2013) CrossRef
14.
Zurück zum Zitat Janota, M., Lynce, I., Manquinho, V., Marques-Silva, J.: PackUp: tools for package upgradability solving. J. Satisf. Boolean Model. Comput. 8, 89–94 (2012)MathSciNetMATH Janota, M., Lynce, I., Manquinho, V., Marques-Silva, J.: PackUp: tools for package upgradability solving. J. Satisf. Boolean Model. Comput. 8, 89–94 (2012)MathSciNetMATH
15.
Zurück zum Zitat Juma, F., Hsu, E. I., McIlraith, S. A.: Preference-based planning via MaxSAT. In: Proceedings of Advances in Artificial Intelligence, vol. 7310 of LNCS, pp. 109–120 (2012)CrossRef Juma, F., Hsu, E. I., McIlraith, S. A.: Preference-based planning via MaxSAT. In: Proceedings of Advances in Artificial Intelligence, vol. 7310 of LNCS, pp. 109–120 (2012)CrossRef
16.
Zurück zum Zitat Kim, K., Fainekos, G. E., Sankaranarayanan, S.: On the minimal revision problem of specification automata. International Journal of Robotics Research 34(12), 1515-1535 (2015)CrossRef Kim, K., Fainekos, G. E., Sankaranarayanan, S.: On the minimal revision problem of specification automata. International Journal of Robotics Research 34(12), 1515-1535 (2015)CrossRef
17.
Zurück zum Zitat Kupferman, O., Vardi, M. Y.: Safraless decision procedures. In: Proceedings of IEEE Annual Symposium on Foundations of Computer Science, pp. 531–542 (2005) Kupferman, O., Vardi, M. Y.: Safraless decision procedures. In: Proceedings of IEEE Annual Symposium on Foundations of Computer Science, pp. 531–542 (2005)
18.
Zurück zum Zitat Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Form. Methods Syst. Des. 19(3), 291–314 (2001)CrossRef Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Form. Methods Syst. Des. 19(3), 291–314 (2001)CrossRef
19.
Zurück zum Zitat Lahijanian, M., Almagor, S., Fried, D., Kavraki, L. E., Vardi, M. Y.: This time the robot settles for a cost: a quantitative approach to temporal logic planning with partial satisfaction. In: Proceedings of Association for the Advancement of Artificial Intelligence (2015) Lahijanian, M., Almagor, S., Fried, D., Kavraki, L. E., Vardi, M. Y.: This time the robot settles for a cost: a quantitative approach to temporal logic planning with partial satisfaction. In: Proceedings of Association for the Advancement of Artificial Intelligence (2015)
20.
Zurück zum Zitat Lahijanian, M., Kwiatkowska, M. Z.: Specification revision for Markov decision processes with optimal trade-off. In: Proceedings of IEEE Conference on Decision and Control, pp. 7411–7418, (2016) Lahijanian, M., Kwiatkowska, M. Z.: Specification revision for Markov decision processes with optimal trade-off. In: Proceedings of IEEE Conference on Decision and Control, pp. 7411–7418, (2016)
21.
Zurück zum Zitat Lahijanian, M., Maly, M.R., Fried, D., Kavraki, L.E., Kress-Gazit, H., Vardi, M.Y.: Iterative temporal planning in uncertain environments with partial satisfaction guarantees. IEEE Trans. Robot. 32(3), 583–599 (2016)CrossRef Lahijanian, M., Maly, M.R., Fried, D., Kavraki, L.E., Kress-Gazit, H., Vardi, M.Y.: Iterative temporal planning in uncertain environments with partial satisfaction guarantees. IEEE Trans. Robot. 32(3), 583–599 (2016)CrossRef
22.
Zurück zum Zitat Martins, R., Manquinho, V. M., Lynce, I.: Open-WBO: a modular MaxSAT solver. In: Proceedings of SAT’14, vol. 8561 of LNCS, pp. 438–445 (2014) Martins, R., Manquinho, V. M., Lynce, I.: Open-WBO: a modular MaxSAT solver. In: Proceedings of SAT’14, vol. 8561 of LNCS, pp. 438–445 (2014)
23.
Zurück zum Zitat Park, J. D.: Using weighted MAX-SAT engines to solve MPE. In: Proceedings of American Association for Artificial Intelligence, pp. 682–687 (2002) Park, J. D.: Using weighted MAX-SAT engines to solve MPE. In: Proceedings of American Association for Artificial Intelligence, pp. 682–687 (2002)
24.
Zurück zum Zitat Pnueli, A.: The temporal logic of programs. In: Annual Symposium on Foundations of Computer Science, pp. 46–57. IEEE (1977) Pnueli, A.: The temporal logic of programs. In: Annual Symposium on Foundations of Computer Science, pp. 46–57. IEEE (1977)
25.
Zurück zum Zitat Raman, V., Kress-Gazit, H.: Towards minimal explanations of unsynthesizability for high-level robot behaviors. In: Proceedings of IEEE/RSJ International Conference on Intelligent Robots and Systems, pp. 757–762 (2013) Raman, V., Kress-Gazit, H.: Towards minimal explanations of unsynthesizability for high-level robot behaviors. In: Proceedings of IEEE/RSJ International Conference on Intelligent Robots and Systems, pp. 757–762 (2013)
26.
Zurück zum Zitat Robinson, N., Gretton, C., Pham, D. N., Sattar, A.: Partial weighted MaxSAT for optimal planning. In: Proceedings of Pacific rim international conference on artificial intelligence, pp. 231–243. Springer (2010) Robinson, N., Gretton, C., Pham, D. N., Sattar, A.: Partial weighted MaxSAT for optimal planning. In: Proceedings of Pacific rim international conference on artificial intelligence, pp. 231–243. Springer (2010)
27.
Zurück zum Zitat Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Proceedings of Automated Technology for Verification and Analysis, vol. 4762 of LNCS, pp. 474–488 (2007) Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Proceedings of Automated Technology for Verification and Analysis, vol. 4762 of LNCS, pp. 474–488 (2007)
28.
Zurück zum Zitat Schuppan, V.: Towards a notion of unsatisfiable and unrealizable cores for LTL. Sci. Comput. Program. 77(7–8), 908–939 (2012)CrossRef Schuppan, V.: Towards a notion of unsatisfiable and unrealizable cores for LTL. Sci. Comput. Program. 77(7–8), 908–939 (2012)CrossRef
29.
Zurück zum Zitat Tabuada, P., Neider, D.: Robust linear temporal logic. In: Proceedings of Computer Science Logic, vol. 62 of LIPIcs, pp. 10:1–10:21 (2016) Tabuada, P., Neider, D.: Robust linear temporal logic. In: Proceedings of Computer Science Logic, vol. 62 of LIPIcs, pp. 10:1–10:21 (2016)
30.
Zurück zum Zitat Tomita, T., Ueno, A., Shimakawa, M., Hagihara, S., Yonezaki, N.: Safraless LTL synthesis considering maximal realizability. Acta Inf. 54(7), 655–692 (2017)MathSciNetCrossRef Tomita, T., Ueno, A., Shimakawa, M., Hagihara, S., Yonezaki, N.: Safraless LTL synthesis considering maximal realizability. Acta Inf. 54(7), 655–692 (2017)MathSciNetCrossRef
31.
Zurück zum Zitat Tumova, J., Hall, G. C., Karaman, S., Frazzoli, E., Rus, D.: Least-violating control strategy synthesis with safety rules. In: Proceedings of ACM International Conference on Hybrid Systems: Computation and Control (2013) Tumova, J., Hall, G. C., Karaman, S., Frazzoli, E., Rus, D.: Least-violating control strategy synthesis with safety rules. In: Proceedings of ACM International Conference on Hybrid Systems: Computation and Control (2013)
Metadaten
Titel
Reactive synthesis with maximum realizability of linear temporal logic specifications
verfasst von
Rayna Dimitrova
Mahsa Ghasemi
Ufuk Topcu
Publikationsdatum
09.11.2019
Verlag
Springer Berlin Heidelberg
Erschienen in
Acta Informatica / Ausgabe 1-2/2020
Print ISSN: 0001-5903
Elektronische ISSN: 1432-0525
DOI
https://doi.org/10.1007/s00236-019-00348-4

Weitere Artikel der Ausgabe 1-2/2020

Acta Informatica 1-2/2020 Zur Ausgabe

Premium Partner