pith. machine review for the scientific record. sign in

arxiv: 2605.04657 · v1 · submitted 2026-05-06 · 💻 cs.LO · cs.FL

Recognition: unknown

Logics for Context-free Hyperproperties

Sarah Winter , Martin Zimmermann
Authors on Pith no claims yet

Pith reviewed 2026-05-08 16:46 UTC · model grok-4.3

classification 💻 cs.LO cs.FL
keywords context-free hyperpropertiesvisibly pushdown automatamodel checkingquantifier alternationinformation-flow propertiesHyperLTLdecidabilityrecursive systems
0
0 comments X

The pith

Model checking is decidable for single-alternation formulas in the logic for context-free hyperproperties when stack height depends only on the first quantifier block.

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

The paper introduces a logic for context-free hyperproperties by adding quantification over traces to visibly pushdown automata, analogous to how HyperLTL extends LTL. It proves decidability of model checking for formulas with one quantifier alternation, as long as the automaton stack height is determined exclusively by traces from the first block. This condition is sufficient to capture many information-flow properties from the literature. It also establishes undecidability when the stack can depend on the second block, which covers nearly all cases with additional alternations.

Core claim

Using a game-based approach, the paper shows that model-checking is decidable for formulas with a single quantifier alternation, provided the stack height of the visibly pushdown automaton only depends on the traces bound to the variables of the first quantifier block. A single quantifier alternation suffices to express many information-flow properties studied in the literature. Model-checking is undecidable for formulas with a single quantifier alternation if the stack behavior may depend on the second quantifier block, implying undecidability for almost all fragments with more than one quantifier alternation.

What carries the argument

Visibly pushdown automata extended with trace quantification over multiple variables, reduced to games for model checking when stack height is restricted to depend only on the first quantifier block.

If this is right

  • Single quantifier alternation is enough to express many information-flow properties in recursive systems.
  • Model checking can be performed for these properties using the game-based method.
  • Undecidability results apply immediately when stack height varies with the second block.
  • Most formulas involving multiple quantifier alternations lack decidable model checking.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Verification practitioners could enforce stack-height independence from certain traces to make properties checkable.
  • The approach might generalize to other pushdown-like models for hyperproperties.
  • Bounded variants or approximations could handle cases where the restriction does not hold.
  • Implementation in existing hyperproperty checkers could start with the decidable fragment.

Load-bearing premise

The stack height of the visibly pushdown automaton only depends on the traces bound to the variables of the first quantifier block.

What would settle it

A single quantifier alternation formula together with a visibly pushdown automaton where the stack height depends solely on the first block's traces, yet no terminating procedure decides whether the formula holds on a given system.

Figures

Figures reproduced from arXiv: 2605.04657 by Martin Zimmermann, Sarah Winter.

Figure 1
Figure 1. Figure 1: Development of the stack height during a run. Positions that are steps (that is, onward, the view at source ↗
Figure 2
Figure 2. Figure 2: The ω-VPA recognizing Step and ProperStep. A transition (q, X, a, q′ , γ) is depicted by an edge from q to q ′ labeled by a, X | γ. Here, c, r, and s stand for arbitrary letters from Σc, Σr, and Σs, respectively. All inputs that would yield a prefix with effect zero cannot be processed (i.e., a letter from Σr when the topmost stack symbol is B). Next, let us consider MatchedCallStep⟨u, v, vτ , vη, τ, η⟩. W… view at source ↗
Figure 3
Figure 3. Figure 3: Turning an PDA into an ω-PDA while preserving universality and normalization. A transi￾tion (q, X, a, q′ , γ) is depicted by an edge from q to q ′ labeled by a, X | γ. Here, ∗ represents an arbitrary letter from Σ (but not #!) and † represents an arbitrary letter from Σ ∪ {#}. Furthermore, the thick transition connects every state of A to q ′ s1 . So, let us consider the case where w has at least two #. If… view at source ↗
read the original abstract

We introduce a novel logic for the specification of context-free hyperproperties, which capture, e.g., the flow of information in security-critical recursive systems. Intuitively, the logic extends visibly pushdown automata by quantification over traces, just like HyperLTL, the most important logic for regular hyperproperties, extends LTL by quantification over traces. Using a game-based approach, we show that model-checking is decidable for formulas with a single quantifier alternation, provided the stack height of the visibly pushdown automaton only depends on the traces bound to the variables of the first quantifier block. A single quantifier alternation suffices to express many information-flow properties studied in the literature. Complementarily, we show that model-checking is undecidable for formulas with a single quantifier alternation, if the stack behavior of the visibly pushdown automaton may depend on the second quantifier block. This also implies that model-checking is undecidable for almost all fragments with more than one quantifier alternation.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 3 minor

Summary. The paper introduces a logic for context-free hyperproperties by extending visibly pushdown automata (VPAs) with trace quantifiers, analogous to how HyperLTL extends LTL. It proves that model checking is decidable for single-quantifier-alternation formulas when the VPA stack height depends only on traces bound to the first quantifier block, using a game-based approach. Complementarily, it shows undecidability when stack behavior may depend on the second block, implying undecidability for almost all fragments with more than one alternation. The logic is claimed to express many information-flow properties from the literature.

Significance. If the results hold, the work provides a useful decidable fragment for verifying context-free hyperproperties in recursive systems, which are important for security properties such as information flow in recursive programs. The precise boundary condition on stack dependence, established via explicit game-based reductions and undecidability proofs, clarifies the limits of decidability and offers guidance for both theory and applications. The demonstration that single alternation suffices for many studied properties strengthens the practical relevance.

major comments (2)
  1. [Abstract and §3 (logic definition)] The central decidability claim in the abstract relies on the condition that 'the stack height of the visibly pushdown automaton only depends on the traces bound to the variables of the first quantifier block.' This condition must be formalized precisely in the definition of the logic and the game construction (likely §3–4); without an explicit syntactic or semantic restriction on how stack operations reference quantified traces, it is unclear whether the game reduction remains sound when traces from the second block indirectly influence stack symbols.
  2. [Abstract and undecidability theorem] The undecidability result for the complementary case (stack behavior depending on the second block) is used to conclude undecidability for 'almost all fragments with more than one quantifier alternation.' The reduction must be checked for whether it covers all multi-alternation patterns or leaves open some fragments (e.g., specific patterns of universal/existential blocks); the abstract statement is strong and requires the precise statement of the covered fragments in the main theorem.
minor comments (3)
  1. [§2–3] Notation for the new logic (e.g., how quantifiers interact with VPA transitions) should be introduced with a small running example early in the paper to aid readability.
  2. [§5 (expressiveness)] The paper should include a table or explicit list of the information-flow properties expressible with single alternation, with references to the original papers where those properties were studied.
  3. [§4 (game construction)] Clarify whether the VPA is assumed to be deterministic or nondeterministic in the model-checking game; this affects the complexity statements.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading, positive assessment of the significance, and constructive comments. We address the two major comments point by point below. We will revise the manuscript to improve clarity on the formal restrictions and the precise scope of the undecidability result.

read point-by-point responses

  1. Referee: [Abstract and §3 (logic definition)] The central decidability claim in the abstract relies on the condition that 'the stack height of the visibly pushdown automaton only depends on the traces bound to the variables of the first quantifier block.' This condition must be formalized precisely in the definition of the logic and the game construction (likely §3–4); without an explicit syntactic or semantic restriction on how stack operations reference quantified traces, it is unclear whether the game reduction remains sound when traces from the second block indirectly influence stack symbols.

    Authors: We agree that an explicit formalization strengthens the presentation. Section 3 defines the logic by associating each VPA with the first quantifier block and restricting its stack operations (push/pop symbols and height) to depend only on traces bound to variables in that block. To remove any ambiguity about indirect influences, we will add an explicit syntactic restriction in the logic definition: the VPA's stack alphabet and transition relation are required to reference only variables from the first quantifier block. We will also include a short lemma in §4 confirming that the game construction preserves this restriction, thereby ensuring soundness. The abstract will be updated to reference this formalized condition. revision: yes

  2. Referee: [Abstract and undecidability theorem] The undecidability result for the complementary case (stack behavior depending on the second block) is used to conclude undecidability for 'almost all fragments with more than one quantifier alternation.' The reduction must be checked for whether it covers all multi-alternation patterns or leaves open some fragments (e.g., specific patterns of universal/existential blocks); the abstract statement is strong and requires the precise statement of the covered fragments in the main theorem.

    Authors: The undecidability theorem shows that model checking becomes undecidable as soon as the VPA stack behavior is allowed to depend on any trace from the second quantifier block. For formulas with additional alternations, the proof reduces them to this base case while preserving the dependence on the second block, covering all common quantifier patterns (including alternating universal-existential blocks after the first). No standard multi-alternation fragments are left open under the dependence condition. To address the request for precision, we will revise the theorem statement to enumerate the exact covered fragments and change the abstract phrasing from 'almost all' to 'all fragments with more than one quantifier alternation in which stack behavior may depend on traces from the second or later blocks'. revision: partial

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper establishes decidability of model-checking for single-quantifier-alternation formulas in its new logic when VPA stack height depends only on the first quantifier block, via an explicit game-based reduction, and proves undecidability for the complementary case where stack behavior may depend on the second block. These results rely on standard automata-theoretic constructions and reductions that are independent of the target claims; the stack-height restriction is stated as an explicit hypothesis rather than derived from the logic itself. No self-definitional steps, fitted inputs renamed as predictions, or load-bearing self-citations appear in the derivation chain.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work relies on standard assumptions from automata theory and logic, with the novel contribution being the specific logic definition and analysis.

axioms (2)
  • domain assumption Visibly pushdown automata model context-free behaviors appropriately
    Assumed as the base for the extension.
  • domain assumption Game-based techniques can decide properties under the given restrictions
    Used for the decidability proof.

pith-pipeline@v0.9.0 · 5455 in / 1332 out tokens · 63696 ms · 2026-05-08T16:46:24.684504+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

32 extracted references

  1. [1]

    Madhusudan

    Rajeev Alur and P. Madhusudan. Visibly pushdown languages. In L´ aszl´ o Babai, editor,STOC 2004, pages 202–211. ACM, 2004

    2004

  2. [2]

    Stack-aware hyperproperties

    Ali Bajwa, Minjian Zhang, Rohit Chadha, and Mahesh Viswanathan. Stack-aware hyperproperties. In Sriram Sankaranarayanan and Natasha Sharygina, editors,TACAS 2023, Part I, LNCS, pages 308–325. Springer, 2023

    2023

  3. [3]

    Prophecy variables for hyperproperty verification

    Raven Beutner and Bernd Finkbeiner. Prophecy variables for hyperproperty verification. InCSF 2022, pages 471–485, , 2022. IEEE

    2022

  4. [4]

    Reachability analysis of pushdown automata: Application to model-checking

    Ahmed Bouajjani, Javier Esparza, and Oded Maler. Reachability analysis of pushdown automata: Application to model-checking. In Antoni W. Mazurkiewicz and J´ ozef Winkowski, editors,CONCUR 1997, LNCS, pages 135–150. Springer, 1997

    1997

  5. [5]

    Alternating automata and a temporal fixpoint calculus for visibly pushdown lan- guages

    Laura Bozzelli. Alternating automata and a temporal fixpoint calculus for visibly pushdown lan- guages. In Lu´ ıs Caires and Vasco Thudichum Vasconcelos, editors,CONCUR 2007, LNCS, pages 476–491. Springer, 2007

    2007

  6. [6]

    Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K

    Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and C´ esar S´ anchez. Temporal logics for hyperproperties. In Mart´ ın Abadi and Steve Kremer, editors,POST 2014, volume 8414 ofLNCS, pages 265–284, , 2014. Springer

    2014

  7. [7]

    Clarkson and Fred B

    Michael R. Clarkson and Fred B. Schneider. Hyperproperties.J. Comput. Secur., 18(6):1157–1210, 2010

    2010

  8. [8]

    Verifying hyperliveness

    Norine Coenen, Bernd Finkbeiner, C´ esar S´ anchez, and Leander Tentrup. Verifying hyperliveness. In Isil Dillig and Serdar Tasiran, editors,CAV 2019, Part I, volume 11561 ofLNCS, pages 121–139, , 2019. Springer

    2019

  9. [9]

    Cohen and Arie Y

    Rina S. Cohen and Arie Y. Gold. Theory of omega-languages. II. A study of various models of omega-type generation and recognition.J. Comput. Syst. Sci., 15(2):185–208, 1977

    1977

  10. [10]

    Cohen and Arie Y

    Rina S. Cohen and Arie Y. Gold. Omega-computations on deterministic pushdown machines.J. Comput. Syst. Sci., 16(3):275–300, 1978

    1978

  11. [11]

    Kuijer, Patrick Totzke, and Martin Zimmermann

    Marie Fortin, Louwe B. Kuijer, Patrick Totzke, and Martin Zimmermann. HyperLTL satisfiability is highly undecidable, HyperCTL ∗ is even harder.Log. Methods Comput. Sci., 21(1):3, 2025

    2025

  12. [12]

    Realizable and context-free hyperlanguages

    Hadar Frenkel and Sarai Sheinvald. Realizable and context-free hyperlanguages. In Pierre Ganty and Dario Della Monica, editors,GandALF 2022, EPTCS, pages 114–130, 2022

    2022

  13. [13]

    Greibach

    Sheila A. Greibach. A new normal-form theorem for context-free phrase structure grammars.J. ACM, 12(1):42–52, 1965

    1965

  14. [14]

    Springer, 2002

    Erich Gr¨ adel, Wolfgang Thomas, and Thomas Wilke, editors.Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 ofLNCS. Springer, 2002

    2002

  15. [15]

    Deciding asynchronous hyper- properties for recursive programs.Proc

    Jens Oliver Gutsfeld, Markus M¨ uller-Olm, and Christoph Ohrem. Deciding asynchronous hyper- properties for recursive programs.Proc. ACM Program. Lang., 8(POPL):33–60, 2024

    2024

  16. [16]

    Hopcroft, Rajeev Motwani, and Jeffrey D

    John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman.Introduction to Automata Theory, Languages, and Computation (3rd Edition). Addison-Wesley Longman Publishing Co., Inc., USA, 2006

    2006

  17. [17]

    Lower bounds for natural proof systems

    Dexter Kozen. Lower bounds for natural proof systems. InFOCS 1977, pages 254–266. IEEE Computer Society, 1977

    1977

  18. [18]

    On the complexity ofω-pushdown automata.Sci

    Yusi Lei, Fu Song, Wanwei Liu, and Min Zhang. On the complexity ofω-pushdown automata.Sci. China Inf. Sci., 60(11):112102:1–112102:15, 2017. 12

    2017

  19. [19]

    Madhusudan, and Olivier Serre

    Christof L¨ oding, P. Madhusudan, and Olivier Serre. Visibly pushdown games. In Kamal Lodaya and Meena Mahajan, editors,FSTTCS 2004, volume 3328 ofLNCS, pages 408–420. Springer, 2004

    2004

  20. [20]

    The keys to decidable HyperLTL satisfiability: Small models or very simple formulas

    Corto Mascle and Martin Zimmermann. The keys to decidable HyperLTL satisfiability: Small models or very simple formulas. In Maribel Fern´ andez and Anca Muscholl, editors,CSL 2020, volume 152 ofLIPIcs, pages 29:1–29:16, , 2020. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik

    2020

  21. [21]

    Noninterference and the composability of security properties

    Daryl McCullough. Noninterference and the composability of security properties. InSSP 1988, pages 177–186, , 1988. IEEE Computer Society

    1988

  22. [22]

    Pebbling mountain ranges and its application of DCFL-recognition

    Kurt Mehlhorn. Pebbling mountain ranges and its application of DCFL-recognition. In J. W. de Bakker and Jan van Leeuwen, editors,ICALP 1980, LNCS, pages 422–435. Springer, 1980

    1980

  23. [23]

    The temporal logic of programs

    Amir Pnueli. The temporal logic of programs. InFOCS 1977, pages 46–57, , Oct 1977. IEEE

    1977

  24. [24]

    Model-checking HyperLTL for pushdown systems

    Adrien Pommellet and Tayssir Touili. Model-checking HyperLTL for pushdown systems. In Mar´ ıa- del-Mar Gallardo and Pedro Merino, editors,SPIN 2018, LNCS, pages 133–152. Springer, 2018

    2018

  25. [25]

    Rabe.A temporal logic approach to information-flow control

    Markus N. Rabe.A temporal logic approach to information-flow control. PhD thesis, Saarland University, 2016

    2016

  26. [26]

    Prasad Sistla and Edmund M

    A. Prasad Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733–749, 1985

    1985

  27. [27]

    Prophecies all the way: Game-based model-checking for HyperQPTL beyond∀ ∗∃∗

    Sarah Winter and Martin Zimmermann. Prophecies all the way: Game-based model-checking for HyperQPTL beyond∀ ∗∃∗. In Patricia Bouyer and Jaco van de Pol, editors,CONCUR 2025, volume 348 ofLIPIcs, pages 37:1–37:18. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik, 2025

    2025

  28. [28]

    Tracy, traces, and transducers: computable counterexam- ples and explanations for HyperLTL model-checking.Acta Informatica, 62(3):31, 2025

    Sarah Winter and Martin Zimmermann. Tracy, traces, and transducers: computable counterexam- ples and explanations for HyperLTL model-checking.Acta Informatica, 62(3):31, 2025. Appendix Before we present the proofs omitted in the main part, we briefly review the closure properties of ω-VPA, as these will be useful throughout the appendix. Let Σ be partitio...

    2025

  29. [29]

    HyperPDA model-checking forΣ 1 formulas is inExpTimeandPSpace-hard

  30. [30]

    13 Proof.1.) We haveT|=∃π 0

    HyperPDA model-checking forΠ 1 formulas is undecidable. 13 Proof.1.) We haveT|=∃π 0. . . .∃π k−1.Aif and only if {mrg(t0, . . . , tk−1)|t 0, . . . , tk−1 ∈L(T)} ∩L(A)̸=∅. As the set on the left-hand side of the intersection isω-regular, i.e., recognized by some B¨ uchi automaton (see, e.g., [14] for definitions), and languages ofω-PDA are effectively clos...

  31. [31]

    expensive

    Verifier winsG(L(A,T,P))if and only ifT|=∀π.∃π ′.A. The proof is split into several independent steps: •In Subsection 8.1, we first show that each individual prophecy is recognized by anω-VPA and bound the size of these automata (lemma 2). Using theω-VPA for the prophecies, we then construct an ω-VPA for the winning conditionL(A,T,P) and bound its size (l...

  32. [32]

    Step”-prophecy it is depends on the type oft(i) and whetherx ProperStep ∈P(i). Hence, the prophecy variable for some “Step

    The resultr·r ′ is defined as expected. Furthermore, letcbe a configuration ofA,v∈Va vertex ofT, andt∈Σ ω. We define opt⟨c, v, t⟩= min r FirstAcc(r), whererranges over accepting runs ofAstarting with configurationcand processing mrg(t, t ′), where t′ ∈L(T Succ(v)). If there is no such accepting run, then opt⟨c, v, t⟩=∞. Lemma 4.Letmrg(α, β)be an outcome o...