@inproceedings{LuoSatBasedQuantifiedSymmetric,
 title = {SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols: An Update},
 author = {Luo, Yun-Rong
and Goel, Aman
and Sakallah, Karem},
 year = {2024},
 isbn = {978-3-031-75380-0},
 booktitle = {Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification},
 editor = {Margaria, Tiziana
and Steffen, Bernhard},
 pages = {374--384},
 publisher = {Springer Nature Switzerland},
 address = {Cham},
 abstract = {In prior work [13], 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 [24], beyond certain cutoff sizes of its sorts. The paper discusses several issues in previous work [13] and provides more succinct FOL formulas of the reachable states for a collection of common protocols.},
 doi = {10.1007/978-3-031-75380-0_21}
}