LuoSatBasedQuantifiedSymmetric:
  type: article
  title: 'SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols: An Update'
  author:
  - Luo, Yun-Rong
  - Goel, Aman
  - Sakallah, Karem
  date: 2024
  editor:
  - Margaria, Tiziana
  - Steffen, Bernhard
  page-range: 374-384
  serial-number:
    doi: 10.1007/978-3-031-75380-0_21
    isbn: 978-3-031-75380-0
  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.'
  parent:
    type: proceedings
    title: Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification
    publisher:
      name: Springer Nature Switzerland
      location: Cham