On Communicating Finite-State Machines

From MaRDI portal
Publication:3657436

DOI10.1145/322374.322380zbMath0512.68039OpenAlexW2025970201WikidataQ56533331 ScholiaQ56533331MaRDI QIDQ3657436

Daniel Brand, Pitro Zafiropulo

Publication date: 1983

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/322374.322380



Related Items

Timed hyperproperties, Relating two automata-based models of orchestration and choreography, Reachability problems on reliable and lossy queue automata, Synchronizability for Verification of Asynchronously Communicating Systems, Forward analysis and model checking for trace bounded WSTS, Realizability of high-level message sequence charts: closing the gaps, Parameterized Verification of Communicating Automata under Context Bounds, Computation in networks of passively mobile finite-state sensors, Communicating finite state machines and an extensible toolchain for multiparty session types, An analysis of the nonemptiness problem for classes of reversal-bounded multicounter machines, Unnamed Item, On the diversity of asynchronous communication, On the analysis of cooperation and antagonism in networks of communicating processes, The complexity of reachability in distributed communicating processes, UNDECIDABILITY AND HIERARCHY RESULTS FOR PARALLEL COMMUNICATING FINITE AUTOMATA, ON THE COMPUTATIONAL CAPACITY OF PARALLEL COMMUNICATING FINITE AUTOMATA, Static analysis of Biological Regulatory Networks dynamics using abstract interpretation, A Normalized Form for FIFO Protocols Traces, Application to the Replay of Mode-based Protocols, Compliance in Behavioural Contracts: A Brief Survey, Multiparty session types, beyond duality, Complexity of reachability problems for finite discrete dynamical systems, Automated verification of automata communicating via FIFO and bag buffers, On deciding synchronizability for asynchronously communicating systems, Orchestrated session compliance, A methodology for constructing communication protocols with multiple concurrent functions, The transformation monoid of a partially lossy queue, Pengines: Web Logic Programming Made Easy, Undecidability of asynchronous session subtyping, A controller synthesis framework for automated service composition, Resolution-based approach to compatibility analysis of interacting automata, Communicating Finite-State Machines and Two-Variable Logic, Automata and Logics for Concurrent Systems: Five Models in Five Pages, Complexity of multi-head finite automata: origins and directions, Handling infinitely branching well-structured transition systems, An interface theory for service-oriented design, Verification in loosely synchronous queue-connected discrete timed automata., Reachability problems for sequential dynamical systems with threshold functions., Well-abstracted transition systems: Application to FIFO automata., On termination and invariance for faulty channel machines, Mind the Shapes: Abstraction Refinement Via Topology Invariants, Quantifying the Discord: Order Discrepancies in Message Sequence Charts, A generic framework for \(n\)-protocol compatibility checking, Communicating finite-state machines, first-order logic, and star-free propositional dynamic logic, Honesty by Typing, Quasi-static scheduling of communicating tasks, Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations, On the Computational Capacity of Parallel Communicating Finite Automata, The Paths to Choreography Extraction, On the Undecidability of Asynchronous Session Subtyping, Reduction and covering of infinite reachability trees, Temporal logics for concurrent recursive programs: satisfiability and model checking, Trace- and failure-based semantics for responsiveness, Fair refinement for asynchronous session types, Data flow analysis of asynchronous systems using infinite abstract domains, Tuning distributed control algorithms for optimal functioning, An abstract framework for choreographic testing, Heterogeneous and asynchronous networks of timed systems, Muller message-passing automata and logics, Process calculi as a tool for studying coordination, contracts and session types, Event clock message passing automata: a logical characterization and an emptiness checking algorithm, Testing for unboundedness of fifo channels, Composition and decomposition of multiparty sessions, A core model for choreographic programming, Communicating processes, scheduling, and the complexity of nontermination, Conversation protocols: a formalism for specification and verification of reactive electronic services, A modular framework for verifying versatile distributed systems, Realisability of pomsets, Connecting open systems of communicating finite state machines, Infinite-state high-level MSCs: model-checking and realizability, Quantitative analysis of probabilistic lossy channel systems, A Kleene theorem and model checking algorithms for existentially bounded communicating automata, Simulating perfect channels with probabilistic lossy channels, Message-passing automata are expressively equivalent to EMSO logic, A general approach to comparing infinite-state systems with their finite-state specifications, An analytical model for end-to-end communication channel over PLCN based on QBDs, Reversible parallel communicating finite automata systems, Realizable temporal logics for web service choreography, Verification of Parameterized Communicating Automata via Split-Width, Automata for Analysing Service Contracts, An Automaton over Data Words That Captures EMSO Logic, Verifying identical communicating processes is undecidable, A contracting model for flexible distributed scheduling, A Gentle Introduction to Multiparty Asynchronous Session Types, Abstract Interpretation of FIFO Replacement, Boundedness, empty channel detection, and synchronization for communicating finite automata, Modal Interface Theories for Communication-Safe Component Assemblies, Realizable causal-consistent reversible choreographies for systems with first-in-first-out communication channels, Input urgent semantics for asynchronous timed session types, A note on the attractor-property of infinite-state Markov chains, Some complexity results for stateful network verification, Verification of probabilistic systems with faulty communication, Verification of programs with half-duplex communication, Moving from interface theories to assembly theories, Verifying lossy channel systems has nonprimitive recursive complexity., Algorithmic analysis of programs with well quasi-ordered domains., Exposure to deadlock for communicating processes is hard to detect, Non-deterministic transducer models of retransmission protocols over noisy channels, Research on the dynamic reconfiguration of Web application using two-phase compatibility verification, Analysis of a class of communicating finite state machines, Guessing the buffer bound for k-synchronizability, Precise Subtyping for Asynchronous Multiparty Sessions, Event-B-Supported Choreography-Defined Communicating Systems, Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types, The inclusion structure of partially lossy queue monoids and their trace submonoids, Reasoning about knowledge and messages in asynchronous multi-agent systems, Rational, recognizable, and aperiodic partially lossy queue languages, Unnamed Item, Composition of synchronous communicating systems, Guessing the Buffer Bound for k-Synchronizability, Communication complexity meets cellular automata: necessary conditions for intrinsic universality, On Composing Communicating Systems, A Theory of Formal Choreographic Languages, A model of actors and grey failures, Branching pomsets: design, expressiveness and applications to choreographies, Asynchronous communicating cellular automata: formalization, robustness and equivalence, Can we communicate? Using dynamic logic to verify team automata, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Propositional Dynamic Logic for Message-Passing Systems, Unnamed Item, Unnamed Item, Mixing Lossy and Perfect Fifo Channels, A Sound Algorithm for Asynchronous Session Subtyping, Verification of Flat FIFO Systems, Diagnosis of Deep Discrete-Event Systems, QUANTIFYING THE DISCORD: ORDER DISCREPANCIES IN MESSAGE SEQUENCE CHARTS, Agent-Based Modeling, Mathematical Formalism for, Progress-preserving Refinements of CTA, Distributed Control of Discrete-Event Systems: A First Step, Assembly Theories for Communication-Safe Component Systems, Global progress for dynamically interleaved multiparty sessions, Well-structured transition systems everywhere!, Unnamed Item, Analysis of Realizability Conditions for Web Service Choreographies, Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness, Automata and Logics for Timed Message Sequence Charts, Unnamed Item, Non axiomatisability of positive relation algebras with constants, via graph homomorphisms, Unnamed Item, Unnamed Item, Model-checking Timed Temporal Logics, Boundedness, hierarchy of fairness, and communication networks with delay, On Communicating Finite-State Machines, Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations, Undecidable verification problems for programs with unreliable channels



Cites Work