Concurrent constraint automata
Laurent Fribourg, Marcos Veloso Peixoto · 1993
We address the problem of the specification and the proof of properties of concurrent systems which manipulate an unbounded number of data. We propose an approach based on an extended notion of automata, called "Concurrent Constraint Automata (CCA)". A CCA is an automaton with constraints and synchronous communication. By automata with constraints, we mean a state machine whose actions and states contain parameters that take their value in the set of natural numbers. With each transition is associated an arithmetic constraint that must be satisfied by the the action and states parameters for enabling the transition. The synchronous communication is realized by means of a handshaking mechanism: two actions are executed simultaneously, their parameters being equalized. Each CCA will be represented as a logic program with arithmetic constraints. Using bottom-up evaluation techniques, we will show that, for a certain class of constraints, the language inclusion problem is decidable: given...