1 Search Results for "Gazda, Maciej"

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.130
Logical Characterisation of Hybrid Conformance

Authors: Maciej Gazda and Mohammad Reza Mousavi

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

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.
Cite as

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)

Copy BibTex To Clipboard

@InProceedings{gazda_et_al:LIPIcs.ICALP.2020.130,
  author =	{Gazda, Maciej and Mousavi, Mohammad Reza},
  title =	{{Logical Characterisation of Hybrid Conformance}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{130:1--130:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.130},
  URN =		{urn:nbn:de:0030-drops-125377},
  doi =		{10.4230/LIPIcs.ICALP.2020.130},
  annote =	{Keywords: Logical Characterisation, Metric Temporal Logic, Conformance, Behavioural Equivalence, Hybrid Systems, Relaxation}
}
  • Refine by Author
  • 1 Gazda, Maciej
  • 1 Mousavi, Mohammad Reza

  • Refine by Classification
  • 1 Software and its engineering → Formal software verification
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 1 Behavioural Equivalence
  • 1 Conformance
  • 1 Hybrid Systems
  • 1 Logical Characterisation
  • 1 Metric Temporal Logic
  • Show More...

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2020

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