Article2378467961: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Johannes Lehmann (Diskussion | Beiträge) (Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Sascha |ErsterAutorNachname=Klüppelholz |FurtherAuthors=Christel Baier}} {{Article |Journal=Science of Computer Programming |Number=6 |Pages=398--425 |Title=Alternating-time stream logic for multi-agent systems |Volume=75 |Year=2010 }} {{Publikation Details |DOI Name=10.1016/J.SCICO.2009.07.007 |Abstract=Constraint automata have been introduced to provide a compositional, operational semantics…“) |
Johannes Lehmann (Diskussion | Beiträge) K (Textersetzung - „Verifikation und formale quantitative Analyse“ durch „Algebraische und logische Grundlagen der Informatik“) |
||
| Zeile 14: | Zeile 14: | ||
|DOI Name=10.1016/J.SCICO.2009.07.007 | |DOI Name=10.1016/J.SCICO.2009.07.007 | ||
|Abstract=Constraint automata have been introduced to provide a compositional, operational semantics for the exogenous coordination language Reo, but they can also serve interface specification for components and an operational model for other coordination languages. Constraint automata have been used as basis for equivalence checking and model checking temporal logical properties. The main contribution of this paper is to reason about the local view and interaction and cooperation facilities of individual components or coalitions of components by means of a multi-player semantics for constraint automata. We introduce a temporal logic framework that combines classical features of alternating-time logic (ATL) for concurrent games with special operators to specify the observable data flow at the I/O-ports of components. Since constraint automata support any kind of synchronous and asynchronous peer-to-peer communication, the resulting game structure is non-standard and requires a series of nontrivial adaptations of the ATL model checking algorithm. | |Abstract=Constraint automata have been introduced to provide a compositional, operational semantics for the exogenous coordination language Reo, but they can also serve interface specification for components and an operational model for other coordination languages. Constraint automata have been used as basis for equivalence checking and model checking temporal logical properties. The main contribution of this paper is to reason about the local view and interaction and cooperation facilities of individual components or coalitions of components by means of a multi-player semantics for constraint automata. We introduce a temporal logic framework that combines classical features of alternating-time logic (ATL) for concurrent games with special operators to specify the observable data flow at the I/O-ports of components. Since constraint automata support any kind of synchronous and asynchronous peer-to-peer communication, the resulting game structure is non-standard and requires a series of nontrivial adaptations of the ATL model checking algorithm. | ||
|Forschungsgruppe= | |Forschungsgruppe=Algebraische und logische Grundlagen der Informatik | ||
}} | }} | ||
Aktuelle Version vom 5. März 2025, 14:48 Uhr
Alternating-time stream logic for multi-agent systems
Sascha KlüppelholzSascha Klüppelholz, Christel BaierChristel Baier
Sascha Klüppelholz, Christel Baier
Alternating-time stream logic for multi-agent systems
Science of Computer Programming, 75(6):398--425, 2010
Alternating-time stream logic for multi-agent systems
Science of Computer Programming, 75(6):398--425, 2010
- KurzfassungAbstract
Constraint automata have been introduced to provide a compositional, operational semantics for the exogenous coordination language Reo, but they can also serve interface specification for components and an operational model for other coordination languages. Constraint automata have been used as basis for equivalence checking and model checking temporal logical properties. The main contribution of this paper is to reason about the local view and interaction and cooperation facilities of individual components or coalitions of components by means of a multi-player semantics for constraint automata. We introduce a temporal logic framework that combines classical features of alternating-time logic (ATL) for concurrent games with special operators to specify the observable data flow at the I/O-ports of components. Since constraint automata support any kind of synchronous and asynchronous peer-to-peer communication, the resulting game structure is non-standard and requires a series of nontrivial adaptations of the ATL model checking algorithm. - Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science
@article{KB2010,
author = {Sascha Kl{\"{u}}ppelholz and Christel Baier},
title = {Alternating-time stream logic for multi-agent systems},
journal = {Science of Computer Programming},
volume = {75},
number = {6},
year = {2010},
pages = {398--425},
doi = {10.1016/J.SCICO.2009.07.007}
}
