Document Open Access Logo

Robust Linear Temporal Logic

Authors Paulo Tabuada, Daniel Neider

PDF
Thumbnail PDF

File

LIPIcs.CSL.2016.10.pdf
  • Filesize: 0.6 MB
  • 21 pages

Document Identifiers

Author Details

Paulo Tabuada
Daniel Neider

Cite AsGet BibTex

Paulo Tabuada and Daniel Neider. Robust Linear Temporal Logic. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.CSL.2016.10

Abstract

Although it is widely accepted that every system should be robust, in the sense that "small" violations of environment assumptions should lead to "small" violations of system guarantees, it is less clear how to make this intuitive notion of robustness mathematically precise. In this paper, we address the problem of how to specify robustness in temporal logic. Our solution consists of a robust version of the Linear Temporal Logic (LTL) fragment that only contains the always and eventually temporal operators.
Keywords
  • Linear Temporal Logic
  • Robustness

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Shaull Almagor and Orna Kupferman. Latticed-ltl synthesis in the presence of noisy inputs. In FOSSACS 2014, volume 8412 of LNCS, pages 226-241. Springer, 2014. Google Scholar
  2. Rajeev Alur, Aditya Kanade, and Gera Weiss. Ranking automata and games for prioritized requirements. In CAV 2008, volume 5123 of LNCS, pages 240-253. Springer, 2008. Google Scholar
  3. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking (Representation and Mind Series). The MIT Press, 2008. Google Scholar
  4. Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A. Henzinger, and Barbara Jobstmann. Robustness in the presence of liveness. In CAV 2010, volume 6174 of LNCS, pages 410-424. Springer, 2010. Google Scholar
  5. Roderick Bloem, Karin Greimel, Thomas A. Henzinger, and Barbara Jobstmann. Synthesizing robust systems. In FMCAD 2009, pages 85-92. IEEE, 2009. Google Scholar
  6. Swarat Chaudhuri, Sumit Gulwani, and Roberto Lublinerman. Continuity analysis of programs. In POPL 2010, pages 57-70. ACM, 2010. Google Scholar
  7. Alexandre Donzé and Oded Maler. Robust satisfaction of temporal logic over real-valued signals. In FORMATS 2010, volume 6246 of LNCS, pages 92-106. Springer, 2010. Google Scholar
  8. Laurent Doyen, Thomas A. Henzinger, Axel Legay, and Dejan Nickovic. Robustness of sequential circuits. In ACSD 2010, pages 77-84. IEEE, 2010. Google Scholar
  9. Rüdiger Ehlers and Ufuk Topcu. Resilience to intermittent assumption violations in reactive synthesis. In HSCC 2014, pages 203-212. ACM, 2014. Google Scholar
  10. Georgios E. Fainekos and George J. Pappas. Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci., 410(42):4262-4291, 2009. Google Scholar
  11. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of LNCS. Springer, 2002. Google Scholar
  12. B. Jonsson and A. Tarski. Boolean algebras with operators. Part I. American Journal of Mathematics, 73(4):891-939, 1951. Google Scholar
  13. Orna Kupferman and Yoad Lustig. Lattice automata. In VMCAI 2007, volume 4349 of LNCS, pages 199-213. Springer, 2007. Google Scholar
  14. Rupak Majumdar and Indranil Saha. Symbolic robustness analysis. In RTSS 2009, pages 355-363. IEEE, 2009. Google Scholar
  15. Doron Peled and Thomas Wilke. Stutter-invariant temporal properties are expressible without the next-time operator. Information Processing Letters, 63(5):243-246, 1997. Google Scholar
  16. Dominique Perrin and Jean-Eric Pin. Infinite Words, volume 141 of Pure and Applied Mathematics. Elsevier, 2004. Google Scholar
  17. Nir Piterman and Amir Pnueli. Faster solutions of rabin and streett games. In LICS 2006, pages 275-284. IEEE, 2006. Google Scholar
  18. G. Priest. Dualising Intuitionist Logic. Principia, 13(2):165-184, 2009. Google Scholar
  19. Aurélien Rizk, Grégory Batt, François Fages, and Sylvain Soliman. A general computational method for robustness analysis with applications to synthetic gene networks. Bioinformatics, 25(12), 2009. URL: http://dx.doi.org/10.1093/bioinformatics/btp200.
  20. Shmuel Safra. On the complexity of omega-automata. In FOCS 1988, pages 319-327. IEEE, 1988. Google Scholar
  21. P. Tabuada and D. Neider. Robust Linear Temporal Logic, 2015. arXiv:1510.08970. Google Scholar
  22. Paulo Tabuada, Sina Yamac Caliskan, Matthias Rungger, and Rupak Majumdar. Towards robustness for cyber-physical systems. IEEE Trans. Automat. Contr., 59(12):3151-3163, 2014. Google Scholar
  23. Milan Česka, David Šafránek, Sven Dražan, and Luboš Brim. Robustness analysis of stochastic biochemical systems. PLoS ONE, 9(4), 2014. URL: http://dx.doi.org/10.1371/journal.pone.0094553.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact