Advertisement

Maximum Realizability for Linear Temporal Logic Specifications

  • Rayna DimitrovaEmail author
  • Mahsa Ghasemi
  • Ufuk Topcu
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11138)

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.

References

  1. 1.
    Almagor, S., Boker, U., Kupferman, O.: Formally reasoning about quality. J. ACM 63(3), 24:1–24:56 (2016)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Alur, R., Kanade, A., Weiss, G.: Ranking automata and games for prioritized requirements. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 240–253. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-70545-1_23CrossRefGoogle Scholar
  3. 3.
    Baier, C., Katoen, J.-P.: Principles of model checking (2008)Google Scholar
  4. 4.
    Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140–156. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-02658-4_14CrossRefGoogle Scholar
  5. 5.
    Cimatti, A., Roveri, M., Schuppan, V., Tchaltsev, A.: Diagnostic information for realizability. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 52–67. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78163-9_9CrossRefGoogle Scholar
  6. 6.
    Cimatti, A., Roveri, M., Schuppan, V., Tonetta, S.: Boolean abstraction for temporal logic satisfiability. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 532–546. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-73368-3_53CrossRefGoogle Scholar
  7. 7.
    Dimitrova, R., Ghasemi, M., Topcu, U.: Maximum realizability for linear temporal logic specifications. CoRR, abs/1804.00415 (2018)Google Scholar
  8. 8.
    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)CrossRefGoogle Scholar
  9. 9.
    Ehlers, R., Raman, V.: Low-effort specification debugging and analysis. In: Proceedings of SYNT 2014.EPTCS, vol. 157, pp. 117–133 (2014)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Finkbeiner, B., Schewe, S.: Bounded synthesis. STTT 15(5—-6), 519–539 (2013)CrossRefGoogle Scholar
  11. 11.
    Juma, F., Hsu, E.I., McIlraith, S.A.: Preference-based planning via MaxSAT. In: Kosseim, L., Inkpen, D. (eds.) AI 2012. LNCS (LNAI), vol. 7310, pp. 109–120. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-30353-1_10CrossRefGoogle Scholar
  12. 12.
    Kim, K., Fainekos, G.E., Sankaranarayanan, S.: On the minimal revision problem of specification automata. Int. J. Robot. Res. 34(12), 1515–1535 (2015)CrossRefGoogle Scholar
  13. 13.
    Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proceedings of FOCS 2005, pp. 531–542 (2005)Google Scholar
  14. 14.
    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)Google Scholar
  15. 15.
    Lahijanian, M., Kwiatkowska, M.Z.: Specification revision for markov decision processes with optimal trade-off. In: Proceedings of CDC 2016, pp. 7411–7418 (2016)Google Scholar
  16. 16.
    Martins, R., Manquinho, V., Lynce, I.: Open-WBO: a modular MaxSAT solver. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 438–445. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-09284-3_33CrossRefGoogle Scholar
  17. 17.
    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).  https://doi.org/10.1007/978-3-540-75596-8_33CrossRefGoogle Scholar
  18. 18.
    Tabuada, P., Neider, D.: Robust linear temporal logic. In: Proceedings of CSL 2016. LIPIcs, , vol. 62, pp. 10:1–10:21 (2016)Google Scholar
  19. 19.
    Tomita, T., Ueno, A., Shimakawa, M., Hagihara, S., Yonezaki, N.: Safraless LTL synthesis considering maximal realizability. Acta Inform. 54(7), 655–692 (2017)MathSciNetCrossRefGoogle Scholar
  20. 20.
    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)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.University of LeicesterLeicesterUK
  2. 2.University of Texas at AustinAustinUSA

Personalised recommendations