Can we communicate? Using dynamic logic to verify team automata

DOI10.1007/978-3-031-27481-7_9MaRDI QIDQ6174530zbMATH OpenFDO

Authors Maurice H. ter Beek, Guillermina Cledou, Rolf Hennicker, José Proença

Publication date 17 August 2023

Published in Formal Methods (Search for Journal in Brave)

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• A team automaton scenario for the analysis of security properties of communication protocols
• Featured Team Automata
• A calculus for team automata
• Communicating automata
• Vector team automata

Cites work

• scientific article; zbMATH DE number 4110131 (Why is no real title available?)
• scientific article; zbMATH DE number 3688686 (Why is no real title available?)
• scientific article; zbMATH DE number 1979561 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• scientific article; zbMATH DE number 1903369 (Why is no real title available?)
• A generic framework for \(n\)-protocol compatibility checking
• A theory of contracts for web services
• Automata for Specifying and Orchestrating Service Contracts
• Behavioural contracts for a sound assembly of components
• Compatibility in a multi-component environment
• Compatibility properties of synchronously and asynchronously communicating components
• Compliance in behavioural contracts: a brief survey
• Compositionality of safe communication in systems of team automata
• Featured Team Automata
• Modal I/O Automata for Interface and Product Line Theories
• Modeling and analysis of communicating systems
• Modularity for teams of I/O automata
• Moving from interface theories to assembly theories
• On Communicating Finite-State Machines
• On weak modal compatibility, refinement, and the MIO workbench
• Richer interface automata with optimistic and pessimistic compatibility
• Vector team automata

Cited in

(5)

• Compositionality of safe communication in systems of team automata
• Realisability of global models of interaction
• Advancing orchestration synthesis for contract automata
• Research Challenges in Orchestration Synthesis
• A Theory of Formal Choreographic Languages

This page was built for publication: Can we communicate? Using dynamic logic to verify team automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6174530)