2002 | OriginalPaper | Buchkapitel
How to Compose Presburger-Accelerations: Applications to Broadcast Protocols
verfasst von : Alain Finkel, Jérôme Leroux
Erschienen in: FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Finite linear systems are finite sets of linear functions whose guards are defined by Presburger formulas, and whose the squares matrices associated generate a finite multiplicative monoid. We prove that for finite linear systems, the accelerations of sequences of transitions always produce an effective Presburger-definable relation. We then show how to choose the good sequences of length n whose number is polynomial in n although the total number of sequences of length n is exponential in n. We implement these theoretical results in the tool FAST [FAS] (Fast Acceleration of Symbolic Transition systems). FAST computes in few seconds the minimal deterministic finite automata that represent the reachability sets of 8 well-known broadcast protocols.