Decidability of a class of dual communicating finite state machines

Autor:	H. Mountassir
Rok vydání:	1996
Předmět:	Finite-state machine Forcing (recursion theory) Computer science Reachability General Earth and Planetary Sciences Graph (abstract data type) Mutual exclusion Transmission protocol Algorithm Perturbation method General Environmental Science Decidability
Zdroj:	ACM SIGOPS Operating Systems Review. 30:59-66
ISSN:	0163-5980
DOI:	10.1145/230908.230920
Popis:	A number of techniques have been proposed to validate systems of communicating machines which exchange exclusively messages through FIFO channels. The reachability analysis is a well-known and most popular technique implemented in several tools of validation. Two majors questions are discussed : the finiteness of the reachability graph and the state explosion problem. In this paper we clarify a restricted class of dual machines and its applicability of real protocols. Our investigation at the first time concern sufficient conditions to ensure the finiteness of the reachability graph. In the second part of the paper we confirm the results using the fair reachability analysis in which global states are generated by forcing the two machines in equal speeds.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::10fd29bc5109e1530386ed8b6c2fe7ad https://doi.org/10.1145/230908.230920 Zobrazit plný text záznamu