scientific article
From MaRDI portal
zbMath0677.68067MaRDI QIDQ3833630
Mark R. Tuttle, Nancy A. Lynch
Publication date: 1989
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
distributed discrete event systemsinput/output automataleader election algorithmvending machinesconcurrent discrete event systems
Formal languages and automata (68Q45) Abstract data types; algebraic specification (68Q65) Theory of operating systems (68N25)
Related Items
A case study on parametric verification of failure detectors, I/O automata in Isabelle/HOL, Wait-free computing, Modeling and analysis of switching max-plus linear systems with discrete-event feedback, A basic compositional model for spiking neural networks, From interface automata to hypercontracts, Fair must testing for I/O automata, Can we communicate? Using dynamic logic to verify team automata, The inhibition spectrum and the achievement of causal consistency, The BG distributed simulation algorithm, Randomized two-process wait-free test-and-set, A Sound Foundation for the Topological Approach to Task Solvability, General Refinement, Part One: Interfaces, Determinism and Special Refinement, Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms, Deriving Complexity Results for Interaction Systems from 1-Safe Petri Nets, Finite-state concurrent programs can be expressed in pairwise normal form, Secret Swarm Unit Reactive k −Secret Sharing, Unnamed Item, Everything Is PSPACE-Complete in Interaction Systems, Monte Carlo Methods for Process Algebra, Efficient test \& set constructions for faulty shared memory, Mechanizing a process algebra for network protocols, A case study in transformational design of concurrent systems, The computational complexity of scenario-based agent verification and design, Precise specification matching for adaptive reuse in embedded systems, Generalized interface automata with multicast synchronization, Dynamic input/output automata: a formal and compositional model for dynamic systems, Byzantine disk paxos: optimal resilience with Byzantine shared memory, Using logic to solve the submodule construction problem, Highly concurrent logically synchronous multicast, Cones and foci: A mechanical framework for protocol verification, Switched PIOA: parallel composition via distributed scheduling, Correctness proof of a database replication protocol under the perspective of the I/O automaton model, Dynamic load balancing with group communication, Metrics for labelled Markov processes, Petri net based verification of distributed algorithms: An example, A blocking model for reactive objects, Compatibility in a multi-component environment, A framework for viewing atomic events in distributed computations, Processes with infinite liveness requirements, Automata and processes on multisets of communicating objects, Sequential Relational Decomposition, Determining asynchronous test equivalence for probabilistic processes, Solving the at-most-once problem with nearly optimal effectiveness, The refinement calculus of reactive systems, rCOS: Defining Meanings of Component-Based Software Architectures, Formal verification of a leader election protocol in process algebra, An algebraic theory of interface automata, RMR-efficient implementations of comparison primitives using read and write operations, Compositional Specification in Rewriting Logic, Branching vs. Linear Time: Semantical Perspective, A Compositional Semantics for Dynamic Fault Trees in Terms of Interactive Markov Chains, Probabilistic contracts: a compositional reasoning methodology for the design of systems with stochastic and/or non-deterministic aspects, Verification of distributed systems with local-global predicates, Symbolic execution of Reo circuits using constraint automata, Stuttering for abstract probabilistic automata, Modal event-clock specifications for timed component-based design, Information gain of black-box testing, Deadlock-freedom in component systems with architectural constraints, Unnamed Item, Interrupting snapshots and the \(\text{Java}^{\text{TM}}\) size method, Hybrid I/O automata., On the Robustness of (Semi) Fast Quorum-Based Implementations of Atomic Shared Memory, Towards formally specifying and verifying transactional memory, On the Minimisation of Acyclic Models, Automata on Multisets of Communicating Objects, A Formalized Theory for Verifying Stability and Convergence of Automata in PVS, Verifying of interface assertions for infinite state Mealy machines, Hybrid concurrency control for abstract data types, Relational Concurrent Refinement: Automata, Closing the complexity gap between FCFS mutual exclusion and mutual exclusion, Timing-Sensitive Noninterference through Composition, Conditions of contracts for separating responsibilities in heterogeneous systems, Distributed event algebras, Task-structured probabilistic I/O automata, A coded shared atomic memory algorithm for message passing architectures, Weighted modal transition systems, The impact of recovery on concurrency control, Using mappings to prove timing properties, Single-bit messages are insufficient for data link over duplicating channels, Alternating-time stream logic for multi-agent systems, Contexts, refinement and determinism, Optimal deployment of eventually-serializable data services, Partial order reduction for state/event LTL with application to component-interaction automata, The impossibility of boosting distributed service resilience, Natural Specifications Yield Decidability for Distributed Synthesis of Asynchronous Systems, On testing UML statecharts, Partial Order Reduction for State/Event LTL, Refined quorum systems, Toward an algebraic theory of systems, Methodologies for Specification of Real-Time Systems Using Timed I/O Automata, The How and Why of Interactive Markov Chains, A Timed Process Algebra for Wireless Networks with an Application in Routing, Relational concurrent refinement. III: Traces, partial relations and automata, Trade-off results for connection management, Processes with local and global liveness requirements, Recomposable restricted finite state machines: definition and solution approaches, Counting protocols for reliable end-to-end transmission, Commutativity-based locking for nested transactions, Dynamic Reactive Modules, Monadic Sequence Testing and Explicit Test-Refinements, On the refinement of liveness properties of distributed systems, Cross-Checking - Enhanced Over-Approximation of the Reachable Global State Space of Component-Based Systems, State Space Reduction of Linear Processes Using Control Flow Reconstruction, Cooperative computing with fragmentable and mergeable groups, Concrete Process Categories, Paths and Simulations, Modularity for teams of I/O automata, Eventually-serializable data services, Linearizable read/write objects, A verification-driven framework for iterative design of controllers, CCS: it's not fair! Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions, Trade-off results for connection management, Computability and realizability for interactive computations, Testing Systems of Concurrent Black-Boxes—An Automata-Theoretic and Decompositional Approach, Translation Templates to Support Strategy Development in PVS, Validating for Liveness in Hidden Adversary Systems, Compositional State Space Reduction Using Untangled Actions, Virtual partition algorithm in a nested transaction environment and its correctness, A Calculus for Team Automata