On Automata with Boundary

TL;DR

This paper introduces a new theoretical framework for automata with boundary to facilitate the design, analysis, and model checking of distributed systems, including deadlock detection and state space reduction.

Contribution

It develops a novel theory of automata with boundary, including notions of behaviour, design, and simulation, and provides algorithms for model checking and state space reduction.

Findings

Effective deadlock detection algorithm demonstrated

State space reduction improves exhaustive search efficiency

Three practical examples illustrate the theory's application

Abstract

We present a theory of automata with boundary for designing, modelling and analysing distributed systems. Notions of behaviour, design and simulation appropriate to the theory are defined. The problem of model checking for deadlock detection is discussed, and an algorithm for state space reduction in exhaustive search, based on the theory presented here, is described. Three examples of the application of the theory are given, one in the course of the development of the ideas and two as illustrative examples of the use of the theory.