<div class="csl-bib-body">
<div class="csl-entry">Bartocci, E., Henzinger, T. A., Nickovic, D., & Oliveira Da Costa, A. A. (2023). Hypernode Automata. In G. Perez & J.-F. Raskin (Eds.), <i>34th International Conference on Concurrency Theory (CONCUR 2023)</i> (pp. 1–16). Schloss-Dagstuhl - Leibniz Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2023.21</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/191163
-
dc.description.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.
en
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.language.iso
en
-
dc.relation.ispartofseries
Leibniz International Proceedings in Informatics (LIPIcs)
-
dc.subject
Hyperproperties
en
dc.subject
Asynchronous
en
dc.subject
Automata
en
dc.subject
Logic
en
dc.title
Hypernode Automata
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.contributor.affiliation
Institute of Science and Technology Austria, Austria
-
dc.contributor.affiliation
Austrian Institute of Technology, Austria
-
dc.contributor.affiliation
Institute of Science and Technology Austria, Austria
-
dc.contributor.editoraffiliation
University of Antwerp, Belgium
-
dc.contributor.editoraffiliation
Université Libre de Bruxelles, Belgium
-
dc.relation.isbn
978-3-95977-299-0
-
dc.description.startpage
1
-
dc.description.endpage
16
-
dc.relation.grantno
ZK 35-G
-
dc.type.category
Full-Paper Contribution
-
tuw.booktitle
34th International Conference on Concurrency Theory (CONCUR 2023)
-
tuw.container.volume
279
-
tuw.peerreviewed
true
-
tuw.relation.publisher
Schloss-Dagstuhl - Leibniz Zentrum für Informatik
-
tuw.book.chapter
21
-
tuw.project.title
High-dimensional statistical learning: New methods to advance economic and sustainability policies
-
tuw.researchTopic.id
I2
-
tuw.researchTopic.name
Computer Engineering and Software-Intensive Systems
-
tuw.researchTopic.value
100
-
tuw.publication.orgunit
E191-01 - Forschungsbereich Cyber-Physical Systems
-
tuw.publisher.doi
10.4230/LIPIcs.CONCUR.2023.21
-
dc.description.numberOfPages
16
-
tuw.author.orcid
0000-0002-8004-6601
-
tuw.author.orcid
0000-0002-2985-7724
-
tuw.editor.orcid
0000-0002-1200-4952
-
tuw.event.name
34th International Conference on Concurrency Theory, CONCUR 2023
en
tuw.event.startdate
18-09-2023
-
tuw.event.enddate
23-09-2023
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Antwerp
-
tuw.event.country
BE
-
tuw.event.presenter
Oliveira Da Costa, Ana Alexandra
-
tuw.event.track
Single Track
-
wb.sciencebranch
Informatik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.value
100
-
item.fulltext
no Fulltext
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.grantfulltext
none
-
item.cerifentitytype
Publications
-
item.languageiso639-1
en
-
item.openairetype
conference paper
-
crisitem.author.dept
E191-01 - Forschungsbereich Cyber-Physical Systems
-
crisitem.author.dept
Institute of Science and Technology Austria
-
crisitem.author.dept
E191-01 - Forschungsbereich Cyber-Physical Systems
-
crisitem.author.dept
E191-01 - Forschungsbereich Cyber-Physical Systems