2 Search Results for "Nickovic, Dejan"

Document
DOI: 10.4230/LIPIcs.CONCUR.2023.21
Hypernode Automata

Authors: Ezio Bartocci, Thomas A. Henzinger, Dejan Nickovic, and Ana Oliveira da Costa

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
We introduce hypernode automata as a new specification formalism for hyperproperties of concurrent systems. They are finite automata with nodes labeled with hypernode logic formulas and transitions labeled with actions. A hypernode logic formula specifies relations between sequences of variable values in different system executions. Unlike HyperLTL, hypernode logic takes an asynchronous view on execution traces by constraining the values and the order of value changes of each variable without correlating the timing of the changes. Different execution traces are synchronized solely through the transitions of hypernode automata. Hypernode automata naturally combine asynchronicity at the node level with synchronicity at the transition level. We show that the model-checking problem for hypernode automata is decidable over action-labeled Kripke structures, whose actions induce transitions of the specification automata. For this reason, hypernode automaton is a suitable formalism for specifying and verifying asynchronous hyperproperties, such as declassifying observational determinism in multi-threaded programs.
Cite as

Ezio Bartocci, Thomas A. Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. Hypernode Automata. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 21:1-21:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bartocci_et_al:LIPIcs.CONCUR.2023.21,
  author =	{Bartocci, Ezio and Henzinger, Thomas A. and Nickovic, Dejan and Oliveira da Costa, Ana},
  title =	{{Hypernode Automata}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{21:1--21:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.21},
  URN =		{urn:nbn:de:0030-drops-190153},
  doi =		{10.4230/LIPIcs.CONCUR.2023.21},
  annote =	{Keywords: Hyperproperties, Asynchronous, Automata, Logic}
}
Document
DOI: 10.4230/DagRep.9.2.48
Specification Formalisms for Modern Cyber-Physical Systems (Dagstuhl Seminar 19071)

Authors: Jyotirmoy V. Deshmukh, Oded Maler, and Dejan Nickovic

Published in: Dagstuhl Reports, Volume 9, Issue 2 (2019)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 19071 "Specification Formalisms for Modern Cyber-Physical Systems." Specifications play a major role in evaluating behaviors of modern cyber-physical systems (CPS). There is currently no specification language that allows joint description of safety, performance, security, privacy, and reliability aspects of CPS applications. The Dagstuhl seminar brought together researchers and practitioners from formal methods, control theory, machine learning and robotics to discuss the state-of-the-art and open challenges in specifying properties of modern CPS. Special attention was given to exploring the intersection of machine learning and formal specification languages, where formal specifications can serve as a bridge between the world of verification and the world of learning and data-mining.
Cite as

Jyotirmoy V. Deshmukh, Oded Maler, and Dejan Nickovic. Specification Formalisms for Modern Cyber-Physical Systems (Dagstuhl Seminar 19071). In Dagstuhl Reports, Volume 9, Issue 2, pp. 48-72, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{deshmukh_et_al:DagRep.9.2.48,
  author =	{Deshmukh, Jyotirmoy V. and Maler, Oded and Nickovic, Dejan},
  title =	{{Specification Formalisms for Modern Cyber-Physical Systems (Dagstuhl Seminar 19071)}},
  pages =	{48--72},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2019},
  volume =	{9},
  number =	{2},
  editor =	{Deshmukh, Jyotirmoy V. and Maler, Oded and Nickovic, Dejan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.9.2.48},
  URN =		{urn:nbn:de:0030-drops-108581},
  doi =		{10.4230/DagRep.9.2.48},
  annote =	{Keywords: Cyber-physical systems, formal specifications, runtime verification and control}
}
  • Refine by Author
  • 2 Nickovic, Dejan
  • 1 Bartocci, Ezio
  • 1 Deshmukh, Jyotirmoy V.
  • 1 Henzinger, Thomas A.
  • 1 Maler, Oded
  • Show More...

  • Refine by Classification
  • 1 Security and privacy → Logic and verification

  • Refine by Keyword
  • 1 Asynchronous
  • 1 Automata
  • 1 Cyber-physical systems
  • 1 Hyperproperties
  • 1 Logic
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2019
  • 1 2023

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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact