SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols: An Update
Yun-Rong Luo, Aman Goel, Karem Sakallah. In International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), 2024.
Prior work introduced a procedure for deriving minimum formulas in first-order logic (FOL) for the reachable states of a restricted class of multi-sorted distributed protocol specifications: protocols with sorts representing unbounded sets of symmetric (indistinguishable) elements. This paper discusses several issues in previous work and provides more succinct FOL formulas of the reachable states for a collection of common protocols.
Paper and Slides
Abstract
In prior work, we introduced a procedure for deriving minimum formulas in first-order logic (FOL) for the reachable states of a restricted class of multi-sorted distributed protocol specifications: protocols with sorts representing unbounded sets of symmetric (indistinguishable) elements. This paper provides a deeper analysis of this idea that yields additional insights about the oft-cited observation that the behavior of such protocols can be inferred from analyzing relatively small finite instances whereby a protocol’s behavior becomes invariant, i.e. saturates, beyond certain cutoff sizes of its sorts. The paper discusses several issues in previous work and provides more succinct FOL formulas of the reachable states for a collection of common protocols.
Citation
@InProceedings{10.1007/978-3-031-75380-0_21,
author="Luo, Yun-Rong and Goel, Aman and Sakallah, Karem",
editor="Margaria, Tiziana and Steffen, Bernhard",
title="SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols: An Update",
booktitle="Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification",
year="2025",
publisher="Springer Nature Switzerland",
address="Cham",
pages="374--384",
isbn="978-3-031-75380-0"
}