Pith. sign in

REVIEW 4 major objections 4 minor 59 references

How to Win First-Order Safety Games

T0 review · 4 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Solving finite first-order safety games is second-order quantifier elimination, and monadic games have a claimed complete decidability boundary.

desk verdict The FO safety game framework and Hilbert-choice strategy extraction are real contributions, but the advertised complete monadic classification is not proven as stated. read the letter →

arxiv 1908.05964 v2 pith:5V4Z52MM submitted 2019-08-16 cs.LO cs.MA

Helmut Seidl , Christian Müller , Bernd Finkbeiner This is my paper · ORCID
classification cs.LOcs.MA MSC 03B2503B1568Q60
keywords first-ordersafetygamesuniversalinvariantslogicsecond-orderquantifiereliminationmonadicgamesynthesisnoninterferenceweakestprecondition
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper takes first-order transition systems, whose states are finite relational structures, and turns them into two-player safety games in which the reachability player picks the universe and some input predicates while the safety player picks the remaining inputs. Its central claim is that deciding whether the safety player has a winning strategy in a finite game is equivalent to eliminating second-order quantifiers from a formula built by iterating weakest preconditions. For games with only monadic, unary predicates, the paper asserts a complete boundary: safety is undecidable once both players control edges or substitutions use equality or disequality, and decidable in three fragments where one player has no relational control. For general predicates, it concentrates on universal first-order invariants, which cover noninterference, and shows how to check inductiveness and extract winning strategies through second-order quantifier elimination and Hilbert-choice constructions. A solver applies the method to synthesize message contents in leader election and paper-assignment strategies that prevent unwanted disclosure of reports.

What carries the argument

The load-bearing device is the weakest-precondition iteration for FO safety games. For each edge $e$, the operator $JeK^\top$ is $\forall A_e$ when the edge is controlled by the reachability player and $\exists B_e$ when it is controlled by the safety player, applied to the postcondition substituted along the edge; iterating these operators from the assertion $I$ yields formulas $\Psi^{(h)}[v]$ whose validity at the start node characterizes safety. The same operator converts the game into a second-order formula, making quantifier elimination the engine of strategy synthesis. For universal invariants, normal-form rewriting plus Ackermann's lemma gives an explicit weakest Hilbert choice operator $\gamma_k$, and the counting-quantifier normal form for monadic formulas bounds the quantifier rank and yields stabilization in the decidable fragments.

What would settle it

Exhibit a monadic safety game with A-edges but no B-edges, whose substitutions contain no equality or disequality literals, and whose assertion contains a disequality between two bound variables; this satisfies none of the conditions of Theorems 5 through 7. Determining whether safety is decidable for that family would directly test the completeness of the claimed classification.

Watch

Extended reading notes

Core claim

The paper's discovery is an exact bridge between play and proof: a finite first-order safety game is safe exactly when a certain iterated weakest-precondition formula, which existentially quantifies the safety player's relations and universally quantifies the reachability player's relations, is valid. That formula is a second-order formula, so the paper concludes that solving finite FO safety games is inter-reducible with second-order quantifier elimination. On the monadic fragment, where every relation has at most one argument, the paper claims a complete decidability boundary: safety is undecidable whenever both players have edge control or the substitutions contain equalities or disequalities, and decidable for the three fragments in which one player has no relation control and the invariant contains only one polarity of equality literals. For general non-monadic predicates the paper focuses on universal first-order invariants, shows that inductiveness checking reduces to existential SO quantifier elimination, and constructs weakest winning strategies through a second-order Hilbert choice operator when elimination succeeds. The reported solver synthesizes such strategies for leader election and for noninterference in a conference-management workflow.

Load-bearing premise

The paper's headline classification of monadic safety games assumes that the listed undecidable and decidable cases exhaust all monadic games, but the proofs do not show that games falling between the cases, such as no B-edges with assertions containing disequalities between bound variables, are covered.

Editorial extensions

If this is right

  • For finite FO safety games, solving safety is inter-reducible with satisfiability of second-order logic, so any complete SO quantifier-elimination method also yields winning strategies.
  • Monadic games with both A- and B-edges, or with equality or disequality literals in substitutions, are undecidable, so no fully automatic method exists for those fragments.
  • The three decidable monadic fragments can be checked effectively, and finite monadic games admit positional, first-order definable winning strategies that can be computed.
  • For universal invariants, checking inductiveness reduces to satisfiability in the Bernays-Schönfinkel-Ramsey fragment, so existing EPR theorem provers can be used.
  • If every iterate in the weakest-precondition sequence is FO definable and so is their infinite conjunction, then the sequence stabilizes and yields an inductive invariant.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The equivalence to second-order quantifier elimination suggests that any future complete SO elimination algorithm would immediately give complete game solving, and conversely the monadic undecidability results can be read as new undecidability results for SO elimination on monadic formulas with equality or disequality.
  • The residual unclassified monadic cases, such as games with A-edges but no B-edges, substitutions without equality literals, and assertions containing disequalities between bound variables, are natural test cases: settling them would complete or refute the claimed complete classification.
  • The paper's closing observation that synthesized strategies should depend only on secret-independent predicates connects these games to games of incomplete information; the self-composition construction can likely be adapted to history-dependent strategies as well.
  • Theorem 10 implies that failure of fixed-point iteration to terminate is itself evidence that the infinite conjunction is not FO definable, offering an algorithmic route to proving non-definability results.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 4 minor

Summary. The paper generalizes first-order transition systems to two-player FO safety games, in which reachability player A chooses a universe, control-flow, and A-controlled predicates, while safety player B chooses B-controlled predicates. The main theoretical contributions are: (i) a weakest-precondition iteration for FO safety games (Theorem 2) and an inter-reduction of finite-game safety to SO satisfiability (Theorem 3); (ii) a claimed complete classification of monadic FO safety games into decidable and undecidable cases (Theorems 4–7); and (iii) for general (non-monadic) FO games, sufficient conditions for deciding inductiveness of universal invariants and for synthesizing weakest FO-definable winning strategies via SO quantifier elimination and a Hilbert choice operator (Theorems 8–12). The paper also reports an implementation, extending the NIWO solver, with experiments on leader election and conference-management benchmarks, including noninterference properties.

Significance. If the classification and the synthesis machinery are correct, the paper makes a useful contribution: the connection between solving FO safety games and SO quantifier elimination (Theorem 3) is elegant, the positional-strategy result (Lemma 1) is cleanly adapted, and the Hilbert-choice characterization (Lemmas 6–7 and Theorem 12) provides a principled way to extract weakest strategies. The software artifact and the benchmark experiments are concrete strengths, and the core fixed-point and Hilbert-choice proofs in the appendix are largely coherent. The main reservation is that the headline 'complete classification' for monadic games is not supported by the theorems as stated; the current formulation contains both an exhaustiveness gap and an internal overlap between the claimed undecidable and decidable classes. These issues are repairable but affect a central claim.

major comments (4)
  1. [Theorem 4 and Theorems 6–7] As printed, the undecidability conditions of Theorem 4(2)/(3) overlap with the decidable classes of Theorems 6 and 7. A substitution such as P(y):=A(y)∧y=c with c∈C contains an equality literal, which would trigger Theorem 4(2), yet such literals are explicitly permitted by Theorem 6(2) and Theorem 7(2). The proof in Appendix C only uses equalities between bound variables (e.g., x1=x2 in the replacement for B). The theorem statements must be qualified (e.g., 'equalities or disequalities between bound variables in substitutions') or otherwise reconciled to eliminate the contradiction.
  2. [Section 4 (abstract and conclusion claim of complete classification)] The abstract and Section 4 ('In summary...') claim a complete classification of monadic FO safety games, but Theorems 4–7 do not prove exhaustiveness. For example, take RA={A}, RB=∅, a single A-edge with the equality-free substitution P(y):=A(y), and an assertion I[v]=∀x∀y.(P(x)∧P(y)→x≠y) at the endpoint. This game violates Theorem 6(1) (disequality between bound variables in I), does not satisfy Theorem 4(2) (substitution contains no equality/disequality), and is outside Theorems 5 and 7 because RA≠∅. No theorem determines whether such residual games are decidable or undecidable. The complete-classification claim therefore requires either an additional exhaustive case analysis or a suitably weakened formulation.
  3. [Appendix C (proof of Theorem 4(1))] The undecidability proof simulates a multi-counter machine, but the simulation is only spelled out for the increment instruction. The text states 'Decrement by 1 can be simulated analogously' and 'Since counters can also be checked for 0' without giving the corresponding substitutions or the error-flag handling for those instructions. Because the full undecidability argument depends on all three instruction types, the proof is incomplete as written; please provide the explicit decrement and zero-test simulations.
  4. [Corollary 1 (proof of Theorem 6)] The proof of Theorem 6 relies on Corollary 1, which asserts (ϕ∧ϕ′)♯=ϕ♯∧(ϕ′)♯ and (∀A.ϕ)♯=(∀A.ϕ♯)♯ for monadic formulas with positive equalities. Neither part is proved in the manuscript, and the second identity in particular is not obvious because the abstraction operator (·)♯ is defined by replacing equalities between bound variables with x∼C y, an operation that need not commute with SO quantifier elimination in general. Please add a proof or a reference.
minor comments (4)
  1. [Abstract] The phrase 'conference mangagement system' contains a typo; it should be 'conference management system'.
  2. [Section 7] The sentence 'The weakest strategy that is safe for stubborn agents (...) can can no longer be proven correct' contains a duplicated word 'can'.
  3. [Figure 3] The results table is captioned as a figure but is not referenced as a figure in the text; consider numbering it as a table for clarity.
  4. [Lemma 1] The proof invokes well-ordering of positions and cites Lemma 2.12 of [22]; a brief explanation of why the axiom of choice applies uniformly to the class of all universes would help the reader.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; core reductions are self-contained, with self-citations confined to auxiliary background techniques.

full rationale

The paper's central derivations are constructed in-text from the definitions of the weakest-precondition operator, explicit backward/forward reductions, and independent classical results. Theorem 2 characterizes safety via the iterated weakest preconditions and is proved by induction on path length. Theorem 3 gives a two-way construction: solving a finite game is reduced to an SO satisfiability check, and an arbitrary SO formula is converted into a safety game whose winning condition exactly matches the formula. The monadic decidability results (Theorems 5-7) rely on Behmann's counting-quantifier normal form and on abstraction arguments developed in the appendices, not on a conclusion identical to an assumption. Theorem 4's undecidability is based on a counter-machine simulation with the first statement attributed to Walukiewicz and the equality/disequality variants carried out in Appendix C. The self-citations that do occur, mainly to [24], are used for the noninterference self-composition construction, for a small universal-SO elimination fact (Lemma 3), and for the NIWO abstraction machinery in the implementation. These are either restated in the text, or serve applications and tooling rather than the load-bearing classification claims, and none of them makes a theorem's output equal to its input by construction. The possible gap in the claimed 'complete classification' (Theorems 4-7 do not explicitly prove that their conditions exhaust all monadic games, and Appendix C asserts decrement and zero-test simulations only 'analogously') is a correctness and completeness risk, not a circularity: no theorem's conclusion is shown to be equivalent to its own hypotheses by definition. There is no fitted parameter renamed as a prediction, and no uniqueness theorem is imported solely from the authors' prior work to force the chosen fragment. Accordingly, the paper receives a score of 0 for circularity.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

The paper introduces no new mathematical entities or fitted parameters. Its results are built on standard logical metatheorems and the modeling assumption that FO transition systems with input predicates partitioned into adversarial and cooperative choices faithfully represent protocols and workflows.

assumptions (6)
  • standard math Axiom of choice for well-ordering game positions
    Used in Lemma 1 to well-order the set of positions and obtain positional winning strategies from individual strategies per universe and valuation.
  • standard math Godel compactness theorem
    Used in Theorem 10 to infer that if the infinite conjunction of fixed-point iterates is FO definable, some finite subset already implies it, forcing termination.
  • standard math Counting quantifier normal form for monadic FO logic (Behmann, Wernhard)
    Used in Theorem 5 to bound the quantifier rank of all weakest-precondition formulas and conclude stability of the fixed-point iteration.
  • standard math Bernays-Schonfinkel-Ramsey fragment is decidable
    Used in Theorem 9 and in the implementation via Z3 EPR to decide inductiveness and implication checks for universal invariants.
  • domain assumption The FO safety game model with player A controlling universe and A-predicates captures the relevant synthesis problems
    Underlies the definition of FO safety games and the claim that synthesized strategies enforce safety or noninterference in protocols and workflows.
  • standard math Ackermann's lemma and SO quantifier elimination techniques are sound
    Used in Sections 5 and 6 for eliminating existential second-order quantifiers and constructing Hilbert choice operators, relying on references [1] and [15].

how reviews work

0 comments
Cite this review

Pith. "Pith review of How to Win First-Order Safety Games." pith.science (2026). https://pith.science/paper/5V4Z52MM

@misc{pith2026190805964,
  author       = {Pith},
  title        = {Pith review of: How to Win First-Order Safety Games},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/5V4Z52MM}},
  note         = {Machine review of arXiv:1908.05964}
}
read the original abstract

First-order (FO) transition systems have recently attracted attention for the verification of parametric systems such as network protocols, software-defined networks or multi-agent workflows like conference management systems. Desirable properties of these systems such as functional correctness or noninterference have conveniently been formulated as safety properties. In order to automatically synthesize strategies that enforce safety or noninterference, we generalize FO transition systems to FO safety games. We prove that the existence of a winning strategy of safety player in finite games is in fact, equivalent to second-order quantifier elimination. For the important case of FO games with monadic predicates only, we provide a complete classification into decidable and undecidable cases. For games with non-monadic predicates, we concentrate on universal first-order invariants, since these are sufficient to express a large class of noninterference properties. Based on general techniques for second-order quantifier elimination, we provide abstraction and refinement techniques in order to synthesize FO strategies that enforce safety. We demonstrate the usefulness of our approach by inferring nontrivial FO specifications in a leader election protocol as well as for paper assignment in a conference mangagement system to exclude unappreciated disclosure of reports.

Figures

Figures reproduced from arXiv: 1908.05964 by the authors.

Figure 1
Figure 1. FO safety game for the running leader election example here a ring, is given by the predicates next and ≤, which are appropriately axiomatized. The participating agents communicate via messages through the predicate msg but are only allowed to send messages to the next agent in the ring topology. In the first step, agents can send any message (determined via the input predicate B) to their neighbor. Afterwards they … view at source ↗
Figure 2
Figure 2. FO safety game for the running conference management example update them after reading the other reviews to the same paper. The predicates A1, A2, A3 represent choices by PC members, while the predicate B1 is under control of the PC chair. The operator += adds tuples to a relation instead of replacing all contents. Specifically, Ry¯ += ϕ abbreviates Ry¯ := Ry¯ ∨ ϕ. ut One property to be checked in example 2 is that … view at source ↗
Figure 3
Figure 3. Experimental Results considered angle of attack (see [14] for an in-depth explanation). In the setting of stubborn agents, the attackers try to break the Noninterference property with no specific intent of working together. Here, the solver infers inductive invariants to￾gether with winning FO strategies (where possible) in 5 −7 seconds. The setting of causal agents is inherently more complex as it allows for groups… view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Self-composition of the FO transition system from fig. 2 where we assume that the length of the sequence of variables az¯ matches the rank of the corresponding predicate R. Let T (s) a denote the FO transition system obtained from T for stubborn agents in this way. In …

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

59 extracted references · 54 canonical work pages

  1. [1]

    Mathematische Annalen 110, 390–413 (1935)

    Ackermann, W.: Untersuchungen ¨ uber das Eliminationsproblem der mathematis- chen Logik. Mathematische Annalen 110, 390–413 (1935)

    work page 1935

  2. [2]

    In: Proc

    de Alfaro, L., Roy, P.: Solving games via three-valued abstraction refinement. In: Proc. CONCUR. vol. 4703, pp. 74–89. Springer-Verlag (2007)

    work page 2007

  3. [3]

    In: ACM Sigplan Notices

    Ball, T., Bjørner, N., Gember, A., Itzhaky, S., Karbyshev, A., Sagiv, M., Schapira, M., Valadarsky, A.: Vericon: Towards verifying controller programs in software- defined networks. In: ACM Sigplan Notices. vol. 49, pp. 282–293. ACM (2014)

    work page 2014

  4. [4]

    Mathematische Annalen 86(3-4), 163–229 (1922)

    Behmann, H.: Beitr¨ age zur Algebra der Logik, insbesondere zum Entschei- dungsproblem. Mathematische Annalen 86(3-4), 163–229 (1922)

    work page 1922

  5. [5]

    Springer Sci- ence & Business Media (2001)

    B¨ orger, E., Gr¨ adel, E., Gurevich, Y.: The classical decision problem. Springer Sci- ence & Business Media (2001)

    work page 2001

  6. [6]

    B¨ orger, E., St¨ ark, R.: History and Survey of ASM Research, pp. 343–367. Springer (2003)

    work page 2003

  7. [7]

    B¨ orger, E., St¨ ark, R.: Tool Support for ASMs, pp. 313–342. Springer (2003)

    work page 2003

  8. [8]

    MIT press (1992)

    Brachman, R.J., Levesque, H.J., Reiter, R.: Knowledge representation. MIT press (1992)

    work page 1992

Show all 59 references
  1. [9]

    In: International Work- shop on Verification, Model Checking, and Abstract Interpretation

    Bradley, A.R.: Sat-based model checking without unrolling. In: International Work- shop on Verification, Model Checking, and Abstract Interpretation. pp. 70–87. Springer (2011)

    2011

  2. [10]

    In: International conference on Tools and Algorithms for the Construction and Analysis of Systems

    De Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 337–

  3. [11]

    In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2008

    Dimitrova, R., Finkbeiner, B.: Abstraction refinement for games with incomplete information. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2008. pp. 175–186 (2008)

    2008

  4. [12]

    In: Jurdzi´ nski, M., Niˇ ckovi´ c, D

    Dimitrova, R., Finkbeiner, B.: Counterexample-guided synthesis of observation predicates. In: Jurdzi´ nski, M., Niˇ ckovi´ c, D. (eds.) Formal Modeling and Analysis of Timed Systems. pp. 107–122. Springer Berlin Heidelberg, Berlin, Heidelberg (2012)

    2012

  5. [13]

    In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017

    Finkbeiner, B., M¨ uller, C., Seidl, H., Zalinescu, E.: Verifying security poli- cies in multi-agent workflows with loops. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017. pp. 6...

    2017

  6. [14]

    In: Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA 2016)

    Finkbeiner, B., Seidl, H., M¨ uller, C.: Specifying and verifying secrecy in workflows with arbitrarily many agents. In: Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA 2016). Lecture Notes in Computer Science, vol. 993...

    2016

  7. [15]

    College Publications (2008)

    Gabbay, D.M., Schmidt, R., Szalas, A.: Second Order Quantifier Elimination: Foun- dations, Computational Aspects and Applications. College Publications (2008)

    2008

  8. [16]

    arXiv preprint arXiv:1808.06255 (2018)

    Gurevich, Y.: Evolving algebras 1993: Lipari guide. arXiv preprint arXiv:1808.06255 (2018)

    2018 arXiv

  9. [17]

    In: Proc

    Henzinger, T., Jhala, R., Majumdar, R.: Counterexample-guided control. In: Proc. ICALP’03, LNCS, vol. 2719, pp. 886–902. Springer (2003)

    2003

  10. [18]

    Theoretical Computer Science 412(1-2), 83–96 (2011) 22 H

    Holzer, M., Kutrib, M., Malcher, A.: Complexity of multi-head finite automata: Origins and directions. Theoretical Computer Science 412(1-2), 83–96 (2011) 22 H. Seidl et al

    2011

  11. [19]

    Journal of the ACM (JACM) 64(1), 7 (2017)

    Karbyshev, A., Bjørner, N., Itzhaky, S., Rinetzky, N., Shoham, S.: Property- directed inference of universal invariants or proving their absence. Journal of the ACM (JACM) 64(1), 7 (2017)

    2017

  12. [20]

    In: Gabbay, D.M., Hogger, C.J., Robinson, J.A., Siekmann, J.H

    Leivant, D.: Higher order logic. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A., Siekmann, J.H. (eds.) Handbook of Logic in Artificial Intelligence and Logic Pro- gramming, Volume2, Deduction Methodologies, pp. 229–322. Oxford University Press (1994)

    1994

  13. [21]

    The Journal of Logic Pro- gramming 31(1), 59 – 83 (1997)

    Levesque, H.J., Reiter, R., Lesp´ erance, Y., Lin, F., Scherl, R.B.: GOLOG: A logic programming language for dynamic domains. The Journal of Logic Pro- gramming 31(1), 59 – 83 (1997). https://doi.org/https://doi.org/10.1016/S0743- 1066(96)00121-5

    1997 doi

  14. [22]

    In: Gr¨ adel, E., Thomas, W., Wilke, T

    Mazala, R.: Infinite games. In: Gr¨ adel, E., Thomas, W., Wilke, T. (eds.) Automata, Logics, and Infinite Games, pp. 23–38. LNCS 2500, Springer, Heidelberg

  15. [23]

    In: International Static Analysis Symposium

    McMillan, K.L., Padon, O.: Deductive verification in decidable fragments with Ivy. In: International Static Analysis Symposium. pp. 43–55. Springer (2018)

    2018

  16. [24]

    In: 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9-12, 2018

    M¨ uller, C., Seidl, H., Zalinescu, E.: Inductive invariants for noninterference in multi-agent workflows. In: 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9-12, 2018. pp. 247–261. IEEE (2018). https://doi.org/10.1109/CSF.2018.00025,...

    2018

  17. [25]

    In: ACM SIGPLAN Notices

    Padon, O., Immerman, N., Karbyshev, A., Lahav, O., Sagiv, M., Shoham, S.: Decentralizing SDN policies. In: ACM SIGPLAN Notices. vol. 50, pp. 663–676. ACM (2015)

    2015

  18. [26]

    In: Proc

    Padon, O., Immerman, N., Shoham, S., Karbyshev, A., Sagiv, M.: Decidability of inferring inductive invariants. In: Proc. of the 43rd Annual ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, POPL 2016. pp. 217–231. ACM (2016). https://doi.org/10.1145/2837614.2837640

    2016

  19. [27]

    Proceedings of the ACM on Programming Languages 1(OOPSLA), 108 (2017)

    Padon, O., Losa, G., Sagiv, M., Shoham, S.: Paxos made EPR: decidable reasoning about distributed protocols. Proceedings of the ACM on Programming Languages 1(OOPSLA), 108 (2017)

    2017

  20. [28]

    ACM SIGPLAN Notices 51(6), 614–630 (2016)

    Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verifica- tion by interactive generalization. ACM SIGPLAN Notices 51(6), 614–630 (2016)

    2016

  21. [29]

    In: Classic Papers in Combinatorics, pp

    Ramsey, F.P.: On a problem of formal logic. In: Classic Papers in Combinatorics, pp. 1–24. Springer (2009)

    2009

  22. [30]

    IBM Journal of Research and Development 10(5), 388–394 (1966)

    Rosenberg, A.L.: On multi-head finite automata. IBM Journal of Research and Development 10(5), 388–394 (1966)

    1966

  23. [31]

    Malaysia; Pear- son Education Limited, (2016)

    Russell, S.J., Norvig, P.: Artificial intelligence: a modern approach. Malaysia; Pear- son Education Limited, (2016)

    2016

  24. [32]

    https://doi.org/10.5281/zenodo.3514277, https:// doi.org/10.5281/zenodo.3514277

    Seidl, H., M¨ uller, C., Finkbeiner, B.: How to Win First Order Safety Games - Software Artifact (Oct 2019). https://doi.org/10.5281/zenodo.3514277, https:// doi.org/10.5281/zenodo.3514277

    2019 doi

  25. [33]

    Spielmann, M.: Abstract state machines: verification problems and complexity. Ph.D. thesis, RWTH Aachen University, Germany (2000),http://sylvester.bth. rwth-aachen.de/dissertationen/2001/008/01_008.pdf

    2000

  26. [34]

    In: 2014 Formal Methods in Computer-Aided Design (FMCAD)

    Walker, A., Ryzhyk, L.: Predicate abstraction for reactive synthesis. In: 2014 Formal Methods in Computer-Aided Design (FMCAD). pp. 219–226 (Oct 2014). https://doi.org/10.1109/FMCAD.2014.6987617

    2014

  27. [35]

    In: International Conference on Automated Reasoning with Analytic Tableaux and Related Methods

    Wernhard, C.: Second-order quantifier elimination on relational monadic formulas– a basic method and some less expected applications. In: International Conference on Automated Reasoning with Analytic Tableaux and Related Methods. pp. 253–

  28. [36]

    arXiv preprint arXiv:1712.06868 (2017) A Proof of Theorem 2 Theorem 2

    Wernhard, C.: Heinrich Behmann’s contributions to second-order quantifier elim- ination from the view of computational logic. arXiv preprint arXiv:1712.06868 (2017) A Proof of Theorem 2 Theorem 2. A FO safety game T is safe iff Init→Ψ (h)[v0] holds for all h≥ 0. Proof. First, we...

    2017 arXiv

  29. [38]

    T σ satisfies the noninterference property ϕa; How to Win First-Order Safety Games 27

  30. [39]

    In particular, each admissible winning strategy for the FO safety gameT (s) a gives rise to a strategy for T that enforces noninterference

    T (s) a σ satisfies the safety property ϕ2 a. In particular, each admissible winning strategy for the FO safety gameT (s) a gives rise to a strategy for T that enforces noninterference. Finding a strategy that enforces noninterference, thus turns into the synthe- sis problem fo...

  31. [40]

    there are both A-edges as well as B-edges

  32. [41]

    there are A-edges and substitutions with equalities or disequalities

  33. [42]

    We first consider the case where there are no equalities, but A- as well as B-edges

    there are B-edges and substitutions with equalities or disequalities. We first consider the case where there are no equalities, but A- as well as B-edges. We show how to construct a safety game G such that an automaton M with multiple counters has a run, starting with empty cou...

  34. [43]

    ϕ1 is in liberal CQNF

  35. [44]

    ϕ2 is in strict CQNF

  36. [45]

    all FO variables and predicates in ϕ1,ϕ 2 also occur in ϕ. ⊓ ⊔ We remark that the construction ofϕ1 in liberal CQNF follows the same lines as the construction of ϕ2 where only the step of eliminating dis-equalities between bound variables and free variables is omitted. The tra...

  37. [46]

    there are no disequalities between bound variables in I,

  38. [47]

    Then it is decidable whether T is safe

    in all literals x =y or x⁄=y in Init and substitutions θ, x∈C or y∈C . Then it is decidable whether T is safe. We have: Lemma 11. Letϕ be a FO formula with free variables from C possibly contain- ing equalities or disequalities between bound variables. We construct a formula ϕ...

  39. [48]

    If ψ→ ϕ holds for any other monadic formula ψ without (dis-)equalities between bound variables, then ψ→ϕ♯

  40. [49]

    If the assumptions of lemma 11 are met, ϕ♯ is called the weakest strengthening of ϕ by formulas without equalities

    There exists some d≥ 0 such that for a model s of multiplicity at least d and a valuation ρ, s,ρ|=ϕ♯ iff s,ρ|=ϕ. If the assumptions of lemma 11 are met, ϕ♯ is called the weakest strengthening of ϕ by formulas without equalities. 32 H. Seidl et al. Proof. Assume that ϕ is in pre...

  41. [51]

    Proof (Proof of theorem 6)

    (∀A.ϕ)♯ = (∀A.ϕ♯)♯ With this, we can now prove the initial theorem 6. Proof (Proof of theorem 6). Let Ψ (h) denote the hth iteration of the weakest precondition (1) as defined in section 3. Due to SO Quantifier Elimination as in [4], each formula Ψ (h)[v] is equivalent to a mona...

  42. [52]

    there are no equalities between bound variables in I,

  43. [53]

    Then it is decidable whether T is safe

    in all literals x =y,x⁄=y in Init and substitutions θ, either x∈C or y∈C . Then it is decidable whether T is safe. The proof is analogous to the proof of theorem 6 where the abstraction of equalities now is replaced with an abstraction of disequalities, and corollary 1 is repl...

  44. [54]

    Then ψ→ ϕi for each i

    Let ψ imply ϕ. Then ψ→ ϕi for each i. Therefore, by induction hypothesis, ψ→ ψ♯ i for all i. As a consequence, ψ→ϕ♯. Now assume that ϕ =ϕ1∨ϕ2. Then ϕ♯ =ϕ♯ 1∨ϕ♯

  45. [55]

    Assume for a contradiction that ψ∧¬ (ϕ♯ 1∨ϕ♯

    If ψ implies ϕ, then for each model M variable assignment ρ, there is some i so that M,ρ |= ψ→ ϕi. Assume for a contradiction that ψ∧¬ (ϕ♯ 1∨ϕ♯

  46. [56]

    Then there is some modelM, assignmentρ so thatM,ρ|=ψ∧¬ϕ♯ 1∧¬ϕ♯

    is satisfiable. Then there is some modelM, assignmentρ so thatM,ρ|=ψ∧¬ϕ♯ 1∧¬ϕ♯

  47. [57]

    In particular, there is some i so that M,ρ |= ϕi∧¬ϕ♯ 1∧¬ϕ♯

  48. [58]

    We conclude that M,ρ|=ϕi∧¬ϕ1∧¬ϕ2 holds — contradiction

    By inductive hypothesis, ϕ♯ i→ ϕi holds. We conclude that M,ρ|=ϕi∧¬ϕ1∧¬ϕ2 holds — contradiction. Similar arguments also apply to existential and universal quantification in ϕ. As a consequence, ψ→ϕ♯ holds. Corollary 2. Assume that ϕ,ϕ′ are monadic FO formulas without positive o...

  49. [59]

    (ϕ∧ϕ′)♯ =ϕ♯∧ (ϕ′)♯, and

  50. [60]

    (∃B.ϕ)♯ = (∃B.ϕ♯)♯ G Proof of Lemma 4 Lemma 4. Every universal FO formula ϕ possibly containing occurrences ofB is equivalent to a formula E∧ (∀¯y.F∨B¯y)∧ (∀¯y′.G∨¬B¯y′)∧ (∀¯y¯y′.H∨B¯y∨¬B¯y′) (2) whereE,F,G,H are universal formulas without B. Proof. W.l.o.g., we assume that ϕ ...

  51. [269]

    Springer (2015) How to Win First-Order Safety Games 23

    2015

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.