Skip to main content
Top

2018 | OriginalPaper | Chapter

Maximum Realizability for Linear Temporal Logic Specifications

Authors : Rayna Dimitrova, Mahsa Ghasemi, Ufuk Topcu

Published in: Automated Technology for Verification and Analysis

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Automatic synthesis from linear temporal logic (LTL) specifications is widely used in robotic motion planning and control of autonomous systems. A common specification pattern in such applications consists of an LTL formula describing the requirements on the behaviour of the system, together with a set of additional desirable properties. We study the synthesis problem in settings where the overall specification is unrealizable, more precisely, when some of the desirable properties have to be (temporarily) violated in order to satisfy the system’s objective. We provide a quantitative semantics of sets of safety specifications, and use it to formalize the “best-effort” satisfaction of such soft specifications while satisfying the hard LTL specification. We propose an algorithm for synthesizing implementations that are optimal with respect to this quantitative semantics. Our method builds upon the idea of bounded synthesis, and we develop a MaxSAT encoding which allows for maximizing the quantitative satisfaction of the soft specifications. We evaluate our algorithm on scenarios from robotics and power distribution networks.

Dont have a licence yet? Then find out more about our products and how to get one now:

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 "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!

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!

Literature
1.
3.
go back to reference Baier, C., Katoen, J.-P.: Principles of model checking (2008) Baier, C., Katoen, J.-P.: Principles of model checking (2008)
7.
go back to reference Dimitrova, R., Ghasemi, M., Topcu, U.: Maximum realizability for linear temporal logic specifications. CoRR, abs/1804.00415 (2018) Dimitrova, R., Ghasemi, M., Topcu, U.: Maximum realizability for linear temporal logic specifications. CoRR, abs/1804.00415 (2018)
8.
go back to reference 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 ATVA 2016. LNCS, vol. 9938 (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 ATVA 2016. LNCS, vol. 9938 (2016)CrossRef
9.
go back to reference Ehlers, R., Raman, V.: Low-effort specification debugging and analysis. In: Proceedings of SYNT 2014.EPTCS, vol. 157, pp. 117–133 (2014)MathSciNetCrossRef Ehlers, R., Raman, V.: Low-effort specification debugging and analysis. In: Proceedings of SYNT 2014.EPTCS, vol. 157, pp. 117–133 (2014)MathSciNetCrossRef
10.
go back to reference Finkbeiner, B., Schewe, S.: Bounded synthesis. STTT 15(5—-6), 519–539 (2013)CrossRef Finkbeiner, B., Schewe, S.: Bounded synthesis. STTT 15(5—-6), 519–539 (2013)CrossRef
12.
go back to reference Kim, K., Fainekos, G.E., Sankaranarayanan, S.: On the minimal revision problem of specification automata. Int. J. Robot. Res. 34(12), 1515–1535 (2015)CrossRef Kim, K., Fainekos, G.E., Sankaranarayanan, S.: On the minimal revision problem of specification automata. Int. J. Robot. Res. 34(12), 1515–1535 (2015)CrossRef
13.
go back to reference Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proceedings of FOCS 2005, pp. 531–542 (2005) Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proceedings of FOCS 2005, pp. 531–542 (2005)
14.
go back to reference 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 AAAI 2015 (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 AAAI 2015 (2015)
15.
go back to reference Lahijanian, M., Kwiatkowska, M.Z.: Specification revision for markov decision processes with optimal trade-off. In: Proceedings of CDC 2016, pp. 7411–7418 (2016) Lahijanian, M., Kwiatkowska, M.Z.: Specification revision for markov decision processes with optimal trade-off. In: Proceedings of CDC 2016, pp. 7411–7418 (2016)
18.
go back to reference Tabuada, P., Neider, D.: Robust linear temporal logic. In: Proceedings of CSL 2016. LIPIcs, , vol. 62, pp. 10:1–10:21 (2016) Tabuada, P., Neider, D.: Robust linear temporal logic. In: Proceedings of CSL 2016. LIPIcs, , vol. 62, pp. 10:1–10:21 (2016)
19.
go back to reference Tomita, T., Ueno, A., Shimakawa, M., Hagihara, S., Yonezaki, N.: Safraless LTL synthesis considering maximal realizability. Acta Inform. 54(7), 655–692 (2017)MathSciNetCrossRef Tomita, T., Ueno, A., Shimakawa, M., Hagihara, S., Yonezaki, N.: Safraless LTL synthesis considering maximal realizability. Acta Inform. 54(7), 655–692 (2017)MathSciNetCrossRef
20.
go back to reference Tumova, J., Hall, G.C., Karaman, S., Frazzoli, E., Rus, D.: Least-violating control strategy synthesis with safety rules. In: Proceedings of HSCC 2013 (2013) Tumova, J., Hall, G.C., Karaman, S., Frazzoli, E., Rus, D.: Least-violating control strategy synthesis with safety rules. In: Proceedings of HSCC 2013 (2013)
Metadata
Title
Maximum Realizability for Linear Temporal Logic Specifications
Authors
Rayna Dimitrova
Mahsa Ghasemi
Ufuk Topcu
Copyright Year
2018
DOI
https://doi.org/10.1007/978-3-030-01090-4_27

Premium Partner