@inproceedings{luo2024sat,
   author = {Luo, Yun-Rong and Goel, Aman and Sakallah, Karem},
   title = {{SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols: An Update}},
   booktitle = {International Symposium on Leveraging Applications of Formal Methods (ISoLA 2024)},
   editor = {Margaria, Tiziana and Steffen, Bernhard},
   address = {Crete, Greece},
   publisher = {Springer Nature Switzerland},
   volume = {LNCS 15221},
   pages = {374--384},
   month = {October},
   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.},
   year = {2024},
   doi = {https://doi.org/10.1007/978-3-031-75380-0_21},
}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 2023
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

{"_id":"XWHvgPh9FpQsZrPha","bibbaseid":"luo-goel-sakallah-satbasedquantifiedsymmetricminimizationofthereachablestatesofdistributedprotocolsanupdate-2024","author_short":["Luo, Y.","Goel, A.","Sakallah, K."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Luo"],"firstnames":["Yun-Rong"],"suffixes":[]},{"propositions":[],"lastnames":["Goel"],"firstnames":["Aman"],"suffixes":[]},{"propositions":[],"lastnames":["Sakallah"],"firstnames":["Karem"],"suffixes":[]}],"title":"SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols: An Update","booktitle":"International Symposium on Leveraging Applications of Formal Methods (ISoLA 2024)","editor":[{"propositions":[],"lastnames":["Margaria"],"firstnames":["Tiziana"],"suffixes":[]},{"propositions":[],"lastnames":["Steffen"],"firstnames":["Bernhard"],"suffixes":[]}],"address":"Crete, Greece","publisher":"Springer Nature Switzerland","volume":"LNCS 15221","pages":"374–384","month":"October","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.","year":"2024","doi":"https://doi.org/10.1007/978-3-031-75380-0_21","bibtex":"@inproceedings{luo2024sat,\n author = {Luo, Yun-Rong and Goel, Aman and Sakallah, Karem},\n title = {{SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols: An Update}},\n booktitle = {International Symposium on Leveraging Applications of Formal Methods (ISoLA 2024)},\n editor = {Margaria, Tiziana and Steffen, Bernhard},\n address = {Crete, Greece},\n publisher = {Springer Nature Switzerland},\n volume = {LNCS 15221},\n pages = {374--384},\n month = {October},\n 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.},\n year = {2024},\n doi = {https://doi.org/10.1007/978-3-031-75380-0_21},\n}\n\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 2023\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n","author_short":["Luo, Y.","Goel, A.","Sakallah, K."],"editor_short":["Margaria, T.","Steffen, B."],"key":"luo2024sat","id":"luo2024sat","bibbaseid":"luo-goel-sakallah-satbasedquantifiedsymmetricminimizationofthereachablestatesofdistributedprotocolsanupdate-2024","role":"author","urls":{},"metadata":{"authorlinks":{}},"downloads":0},"bibtype":"inproceedings","biburl":"http://web.eecs.umich.edu/~karem/publications/Sakallah-Publications.bib","dataSources":["dAWPbXiJP4ihEN4GZ"],"keywords":[],"search_terms":["sat","based","quantified","symmetric","minimization","reachable","states","distributed","protocols","update","luo","goel","sakallah"],"title":"SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols: An Update","year":2024}