Synchronizability of communicating finite state machines is not decidable
DOI10.4230/LIPICS.ICALP.2017.122zbMATH Open1442.68138arXiv1702.07213MaRDI QIDQ5111454FDOQ5111454
Authors: Etienne Lozes, Alain Finkel 
Publication date: 27 May 2020
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1702.07213
Recommendations
- On deciding synchronizability for asynchronously communicating systems
- On the decidability of correctness problems for a communicating automata net
- Boundedness, empty channel detection, and synchronization for communicating finite automata
- scientific article; zbMATH DE number 3881887
- Priority Networks of Communicating Finite State Machines
Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Computer science (68-XX)
Cites Work
- Verification of programs with half-duplex communication
- Multiparty session types meet communicating automata
- Deciding choreography realizability
- On Communicating Finite-State Machines
- Mixing Lossy and Perfect Fifo Channels
- Synchronizability for Verification of Asynchronously Communicating Systems
- On deciding synchronizability for asynchronously communicating systems
- Context-Bounded Analysis of Concurrent Queue Systems
- Verification, Model Checking, and Abstract Interpretation
- Reachability analysis of communicating pushdown systems
- Decidable Topologies for Communicating Automata with FIFO and Bag Channels
- A Kleene theorem and model checking algorithms for existentially bounded communicating automata
- A Reduction Theorem for the Verification of Round-Based Distributed Algorithms
- Reduction
- Title not available (Why is that?)
- Automated verification of automata communicating via FIFO and bag buffers
- Automated Analysis of Asynchronously Communicating Systems
- On the completeness of verifying message passing programs under bounded asynchrony
- Realisability of choreographies
Cited In (14)
- A formal theory of choreographic programming
- Input urgent semantics for asynchronous timed session types
- Verification of Flat FIFO Systems
- Branching pomsets: design, expressiveness and applications to choreographies
- Guessing the buffer bound for k-synchronizability
- On the \(k\)-synchronizability of systems
- Title not available (Why is that?)
- Guessing the Buffer Bound for k-Synchronizability
- Weakly synchronous systems with three machines are Turing powerful
- Multiparty half-duplex systems and synchronous communications
- Event-B-Supported Choreography-Defined Communicating Systems
- Automatic analysis of complex interactions in microservice systems
- Towards generalised half-duplex systems
- Title not available (Why is that?)
This page was built for publication: Synchronizability of communicating finite state machines is not decidable
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5111454)
