Document Open Access Logo

Logical Characterisation of Hybrid Conformance

Authors Maciej Gazda, Mohammad Reza Mousavi

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2020.130.pdf
  • Filesize: 0.67 MB
  • 18 pages

Document Identifiers

Author Details

Maciej Gazda
  • Department of Computer Science, University of Sheffield, UK
Mohammad Reza Mousavi
  • School of Informatics, University of Leicester, UK

Acknowledgements

We thank Rayna Dimitrova for her helpful comments on an earlier version of this article. We also thank anonymous ICALP reviewers for their thorough feedback which helped us improve the paper.

Cite As Get BibTex

Maciej Gazda and Mohammad Reza Mousavi. Logical Characterisation of Hybrid Conformance. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 130:1-130:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.ICALP.2020.130

Abstract

Logical characterisation of a behavioural equivalence relation precisely specifies the set of formulae that are preserved and reflected by the relation. Such characterisations have been studied extensively for	exact semantics on discrete models such as bisimulations for labelled transition systems and Kripke structures, but to a much lesser extent for approximate relations, in particular in the context of hybrid systems. We present what is to our knowledge the first characterisation result for approximate notions of hybrid refinement and hybrid conformance involving tolerance thresholds in both time and value. Since the notion of conformance in this setting is approximate, any characterisation will unavoidably involve a notion of relaxation, denoting how the specification formulae should be relaxed in order to hold for the implementation. We also show that an existing relaxation scheme on Metric Temporal Logic used for preservation results in this setting is not tight enough for providing a characterisation of neither hybrid conformance nor refinement. The characterisation result, while interesting in its own right, paves the way to more applied research, as our notion of hybrid conformance underlies a formal model-based technique for the verification of cyber-physical systems.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Software and its engineering → Formal software verification
Keywords
  • Logical Characterisation
  • Metric Temporal Logic
  • Conformance
  • Behavioural Equivalence
  • Hybrid Systems
  • Relaxation

Metrics

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

References

  1. Houssam Abbas, Hans D. Mittelmann, and Georgios E. Fainekos. Formal property verification in a conformance testing framework. Proceedings of MEMOCODE 2014, pages 155-164, 2014. URL: https://doi.org/10.1109/MEMCOD.2014.6961854.
  2. Houssam Y. Abbas. Test-Based Falsification and Conformance Testing for Cyber-Physical Systems. PhD thesis, Arizona State University, 2015. URL: http://hdl.handle.net/2286/R.A.150686.
  3. Samson Abramsky. Observation equivalence as a testing equivalence. Theor. Comput. Sci., 53:225-241, 1987. Google Scholar
  4. Luca Aceto, Anna Ingolfsdottir, Kim Guldstrand Larsen, and Jiri Srba. Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, 2007. URL: https://doi.org/10.1017/CBO9780511814105.
  5. Rajeev Alur, Tomás Feder, and Thomas A. Henzinger. The benefits of relaxing punctuality. J. ACM, 43(1):116-146, 1996. URL: https://doi.org/10.1145/227595.227602.
  6. Rajeev Alur and Thomas A. Henzinger. Real-time logics: Complexity and expressiveness. Information and Computation, 104(1):35-77, 1993. URL: https://doi.org/10.1006/inco.1993.1025.
  7. Bard Bloom, Wan Fokkink, and Rob J. van Glabbeek. Precongruence formats for decorated trace preorders. In 15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, California, USA, June 26-29, 2000, pages 107-118. IEEE Computer Society, 2000. URL: https://doi.org/10.1109/LICS.2000.855760.
  8. Manfred Broy, Bengt Jonsson, Joost-Pieter Katoen, Martin Leucker, and Alexander Pretschner. Model-Based Testing of Reactive Systems, volume 3472 of Lecture Notes in Computer Science. Springer, 2005. Google Scholar
  9. Valentina Castiglioni, Konstantinos Chatzikokolakis, and Catuscia Palamidessi. A logical characterization of differential privacy. Sci. Comput. Program., 188:102388, 2020. URL: https://doi.org/10.1016/j.scico.2019.102388.
  10. Rance Cleaveland and Steve Sims. The NCSU concurrency workbench. In Proceedings of the 8th International Conference on Computer Aided Verification (CAV '96), volume 1102 of Lecture Notes in Computer Science, pages 394-397. Springer, 1996. URL: https://doi.org/10.1007/3-540-61474-5_87.
  11. Thao Dang. Model-based testing of hybrid systems. Monograph in Model-Based Testing for Embedded Systems, CRC Press, 2010. Google Scholar
  12. Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga. Linear and branching system metrics. IEEE Trans. Software Eng., 35(2):258-273, 2009. Google Scholar
  13. Rocco De Nicola and Matthew Hennessy. Testing equivalences for processes. Theor. Comput. Sci., 34:83-133, 1984. URL: https://doi.org/10.1016/0304-3975(84)90113-0.
  14. Josee Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled markov processes. Theor. Comput. Sci., 318(3):323-354, 2004. URL: https://doi.org/10.1016/j.tcs.2003.09.013.
  15. Jyotirmoy V. Deshmukh, Alexandre Donzé, Shromona Ghosh, Xiaoqing Jin, Garvit Juniwal, and Sanjit A. Seshia. Robust online monitoring of signal temporal logic. Formal Methods in System Design, 51(1):5-30, 2017. URL: https://doi.org/10.1007/s10703-017-0286-7.
  16. Jyotirmoy V. Deshmukh, Rupak Majumdar, and Vinayak S. Prabhu. Quantifying conformance using the Skorokhod metric. Formal Methods in System Design, 50(2-3):168-206, 2017. URL: https://doi.org/10.1007/s10703-016-0261-8.
  17. Daniel Gburek and Christel Baier. Bisimulations, logics, and trace distributions for stochastic systems with rewards. In Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (HSCC 2018), pages 31-40. ACM, 2018. Google Scholar
  18. Shromona Ghosh, Dorsa Sadigh, Pierluigi Nuzzo, Vasumathi Raman, Alexandre Donzé, Alberto L. Sangiovanni-Vincentelli, S. Shankar Sastry, and Sanjit A. Seshia. Diagnosis and repair for synthesis from signal temporal logic specifications. In Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, Vienna, Austria, April 12-14, 2016, pages 31-40. ACM, 2016. URL: https://doi.org/10.1145/2883817.2883847.
  19. Antoine Girard, A. Agung Julius, and George J. Pappas. Approximate simulation relations for hybrid systems. Discrete Event Dynamic Systems, 18(2):163-179, 2008. URL: https://doi.org/10.1007/s10626-007-0029-9.
  20. Antoine Girard and George J. Pappas. Approximation metrics for discrete and continuous systems. IEEE Trans. Automat. Contr., 52(5):782-798, 2007. URL: https://doi.org/10.1109/TAC.2007.895849.
  21. Mathew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. J. ACM, 32(1):137-161, 1985. URL: https://doi.org/10.1145/2455.2460.
  22. Narges Khakpour and Mohammad Reza Mousavi. Notions of conformance testing for cyber-physical systems: Overview and roadmap (invited paper). In Proc. of the 26th International Conference on Concurrency Theory, CONCUR 2015, volume 42 of LIPIcs, pages 18-40. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  23. Ron Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems, 2(4):255-299, 1990. URL: https://doi.org/10.1007/BF01995674.
  24. Oded Maler and Dejan Nickovic. Monitoring temporal properties of continuous signals. In Proceedings of the Joint International Conferences on Formal Modelling and Analysis of Timed Systems and Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant (FORMATS and FTRTFT) 2004, volume 3253 of Lecture Notes in Computer Science, pages 152-166. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30206-3_12.
  25. Amir Pnueli. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS 1977), pages 46-57. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  26. Pavithra Prabhakar, Vladimeros Vladimerou, Mahesh Viswanathan, and Geir E. Dullerud. Verifying tolerant systems using polynomial approximations. In Theodore P. Baker, editor, Proceedings of the 30th IEEE Real-Time Systems Symposium, RTSS 2009, Washington, DC, USA, 1-4 December 2009, pages 181-190. IEEE Computer Society, 2009. URL: https://doi.org/10.1109/RTSS.2009.28.
  27. Sriram Sankaranarayanan, Suhas Akshar Kumar, Faye Cameron, B. Wayne Bequette, Georgios E. Fainekos, and David M. Maahs. Model-based falsification of an artificial pancreas control system. SIGBED Review, 14(2):24-33, 2017. URL: https://doi.org/10.1145/3076125.3076128.
  28. Jan Tretmans. Model based testing with labelled transition systems. In Formal Methods and Testing, An Outcome of the FORTEST Network, Revised Selected Papers, volume 4949 of Lecture Notes in Computer Science, pages 1-38. Springer, 2008. Google Scholar
  29. Cumhur Erkan Tuncali, Bardh Hoxha, Guohui Ding, Georgios E. Fainekos, and Sriram Sankaranarayanan. Experience report: Application of falsification methods on the UxAS system. In Proceedings of the 10th International NASA Formal Methods Symposium (NFM 2018), volume 10811 of Lecture Notes in Computer Science, pages 452-459. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-77935-5_30.
  30. Rob J. van Glabbeek. The linear time-branching time spectrum (extended abstract). In Jos C. M. Baeten and Jan Willem Klop, editors, CONCUR '90, Theories of Concurrency: Unification and Extension, Amsterdam, The Netherlands, August 27-30, 1990, Proceedings, volume 458 of Lecture Notes in Computer Science, pages 278-297. Springer, 1990. URL: https://doi.org/10.1007/BFb0039066.
  31. Mihalis Yannakakis and David Lee. Testing of finite state systems. In Proceedings of Computer Science Logic (CSL 1999), volume 1584 of Lecture Notes in Computer Science, pages 29-44. Springer Berlin Heidelberg, 1999. Google Scholar
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 About DROPS Imprint Privacy Contact