Non-Deterministic Planning for Hyperproperty Verification

Venue: icaps-conference_org_ICAPS_2024_Conference
Published: 2023-12-08 09:09:23

Abstract: Non-deterministic planning aims to find a policy that achieves a given objective in an environment where actions have uncertain effects, and the agent - potentially - only observes parts of the current state.
Hyperproperties are properties that relate multiple paths of a system and can, e.g., capture security and information-flow policies.
Popular logics for expressing hyperproperties - such as HyperLTL - extend LTL by offering selective quantification over executions of a system.
In this paper, we show that planning offers a powerful intermediate language for the automated verification of hyperproperties. 
Concretely, we present an algorithm that, given a HyperLTL verification problem, constructs a non-deterministic multi-agent planning instance (in the form of a QDec-POMDP) that, when admitting a plan, implies the satisfaction of the verification problem.
We show that for large fragments of HyperLTL, the resulting planning instance corresponds to a classical, FOND, or POND planning problem.
We implement our encoding in a prototype verification tool and report on encouraging experimental results using off-the-shelf FOND planners.

Main paper: 
 introduction: 
 AI planning is the task of finding a policy (aka. plan) that ensures that a specified goal is reached. In this paper, we present an exciting new application of planning: the automated verification of hyperproperties.Hyperproperties and HyperLTL. Hyperproperties generalize traditional trace properties by relating multiple executions of a system (Clarkson and Schneider 2008) . A trace property -specified, e.g., in LTL -reasons about individual executions in isolation, which falls short in many applications. For example, assume we want to specify that the output of a system (modeled via atomic proposition o) only depends on some low-security input l and does not leak information about a secret input h. We cannot specify this as a trace property in LTL; we need to relate multiple executions to observe how different inputs impact the output. Hyper-LTL extends LTL with explicit quantification over executions (Clarkson et al. 2014) , and allows for the specification of such a property. For example, we can express observational determinism (Zdancewic and Myers 2003) as follows:∀π. ∀π ′ . (l π ↔ l π ′ ) → G(o π ↔ o π ′ ) (OD)This formula states that on any pair of traces π, π ′ with identical low-security input, the output is (globally) the same. In other words, the system is deterministic in the low-security inputs. For non-deterministic systems, (OD) is often too strict, as any given low-security input might lead to multiple outputs. A relaxed notation -called non-inference (NI) (McLean 1994) -can be expressed in HyperLTL as follows:EQUATIONNI) That is, for any execution π, there exists another execution π ′ that has the same low-security behavior (via propositions o, l) , but yet has a fixed "dummy" high-security input (in our case, we require that h is always false, i.e., never holds on π ′ ). If NI holds, a low-security attacker can not distinguish any high-security input from the dummy input.HyperLTL Verification as Planning. Our goal is to automatically verify that a finite-state system T satisfies a HyperLTL formula φ. We introduce a novel verification approach that leverages the advanced methods developed within the planning community. Concretely, we present a reduction that soundly converts a HyperLTL verification problem into a planning problem. Depending on the HyperLTL formula, our encoding uses several advanced features supported by modern planning frameworks, such as uncertain action effects (non-determinism) (Cimatti et al. 2003) , partial observations (Bertoli et al. 2006) , and multiple agents. We show that -by carefully combining these featureswe obtain a planning problem that is sound w.r.t. the Hy-perLTL semantics: every plan can be translated back into a validity witness for the original verification problem. As a consequence, our encoding allows us to utilize mature planning tools for the verification of complex HyperLTL properties. We implement our encoding as a prototype and demonstrate that existing off-the-shelf planners outperform previous game-based verification methods for HyperLTL. 
high-level overview: 
 Before proceeding with a formal construction, we provide some high-level intuition of our encoding. In HyperLTL, we can quantify over the executions of a system (as seen informally in OD and NI). The overarching idea in our encoding is to let the planning agent control all existentially quantified executions, such that any valid plan directly corresponds to a witness for the existentially quantified executions.Verification as Planning. As an example, assume we want to verify that (OD) does not hold on a given system T , i.e., we want to find concrete executions π, π ′ that violate the body of (OD). We can interpret this as a classical (singleagent) planning problem: each planning state maintains two locations in T , one for π and one for π ′ , and, in each step, the actions update the locations for π, π ′ by moving along the transitions in T . The planning objective is to construct executions for π, π ′ that violate(l π ↔ l π ′ ) → G(o π ↔ o π ′ ).Any successful plan (i.e., sequence of transitions) then directly corresponds to concrete paths π, π ′ disproving (OD).Verification as Non-deterministic Planning. Verification becomes more interesting when the HyperLTL formula contains alternations, as in (NI). Following the above intuition, a plan should provide a concrete witness for (the existentially quantified) π ′ , but -this time -we need to consider all executions for (the universally quantified) π. Our idea is that we can approximate this behavior by viewing it as a fullyobservable non-deterministic (FOND) planning problem; intuitively, a plan controls the behavior of π ′ while the behavior of π is non-deterministic. That is, each action determines a successor location for π ′ but also non-deterministically updates the location of π. The agent's object is to ensure that π, π ′ satisfy G (o π ↔ o π ′ ) ∧ (l π ↔ l π ′ ) ∧ ¬h π ′ (the body of NI). Any plan (which is now conditional on the nondeterministic outcomes) thus defines a concrete execution for π ′ , depending on the concrete execution for π.Verification as Planning Under Partial Observations. In (NI), π ′ is quantified after π, so the action sequence that defines the behavior of π ′ can be based on the behavior of π. This changes when quantifiers succeed existential quantification, e.g., in a formula of the form ∃π. ∀π ′ . For such formulas, we follow the same idea as before but ensure that the actions controlling π are independent of the current state of π ′ , i.e., the agent must act under partial information.This intuition generalizes to full HyperLTL by introducing one agent for each existential quantifier and carefully designing the observations of each agent (cf. Section 6). 
related work: 
 Non-deterministic planning provides a powerful intermediate language that encompasses problems such as reactive synthesis (Camacho et al. 2018) , controller synthesis in MDPs, epistemic planning (Engesser and Miller 2020) , and generalized planning (Hu and Giacomo 2011) . Consequently, many methods and tools have been developed (Pereira et al. 2022; Messa and Pereira 2023; Camacho et al. 2017; Mokhtari et al. 2021; Geffner and Geffner 2018; Rodriguez et al. 2021; Muise, McIlraith, and Beck 2012; Kuter et al. 2008) , with some also supporting partial observations (Bertoli et al. 2006; Cimatti et al. 2003; Bonet and Geffner 2011) . In terms of HyperLTL verification, complete verification is possible via expensive automata complementations (Finkbeiner, Rabe, and Sánchez 2015) , or cheaper (but incomplete) bounded methods (Hsu, Sánchez, and Bonakdarpour 2021) . For ∀ * ∃ * HyperLTL properties, our encoding is related to the parity-game-based approach of Beutner and Finkbeiner (2022) , where one player controls existentially quantified executions. Crucially, the size of their game scales exponentially in the number of quantified executions, making it impractical for larger instances. In contrast, the planning-based approach in this paper can describe the problem compactly (locally) and let the planner determine how to best explore the state space. Our experimental results show that this leads to large performance gains in practice (cf. Section 7). Moreover, our planning-based encoding is applicable to arbitrary quantifier prefixes and thus provides a verification method for the full logic, not only ∀ * ∃ * formulas. 
planning preliminaries: 
 As a basic planning model, we use Qualitative Dec-POMDP (QDec-POMDP), a general model that encompasses multiple agents, non-deterministic effects, and partial observations (Brafman, Shani, and Zilberstein 2013) .Definition 1. A QDec-POMDP is a tuple G = (I, S, S 0 , {A i }, δ, {Ω i }, {ω i }, G), where I = {1, . . . , m} is a finite set of agents; S is a finite set of states; and S 0 ⊆ S is a set of initial states; For each i ∈ I, A i is a finite set of actions and we define ⃗ A = ⊗ i∈I A i as the set of joint actions. δ : S × ⃗ A → 2 S is a (non-deterministic) transition function; For each i ∈ I, Ω i is a finite set of observations, and the observation function ω i : S → Ω i gives i's local observation; Lastly, G ⊆ S is a set of goal states.A for the joint action where each agent i ∈ I chooses action a i . A local policy for an agent i ∈ I, is a conditional plan that picks an action based on the history of observations, i.e., a function f i : Ω + i → A i (represented, e.g., as a tree of degree |Ω i | where nodes are labeled with elements from A i ). A joint policy {f i } assigns each agent i ∈ I a local policy f i . A finite path p ∈ S + is compatible with {f i } if and only if (1) p(0) ∈ S 0 (i.e., the path starts in an initial state), and (2) for every0 ≤ k < |p|, p(k + 1) ∈ δ(p(k), {a i }) where a i = f i (ω i (p(0)) • • • ω i (p(k))).That is, in every step, we compute the joint action {a i }, where each a i is determined by policy f i based on the past observations made by i on the prefix p(0) • • • p(k). We write Exec({f i }) ⊆ S + for the set of all {f i }-compatible paths.The objective of the agents is to reach a goal state in G. Following Cimatti et al. (2003) , we distinguish between different levels of reachability. A policy is a weak plan if some p ∈ Exec({f i }) reaches a state in G, i.e., {f i } can reach the goal provided the non-determinism is resolved favorably. A policy is a strong plan if there exists a N ∈ N such that every p ∈ Exec({f i }) with |p| ≥ N reaches G, i.e., the goal is guaranteed to be reached, irrespective of non-deterministic outcomes. Finally, a policy is a strong cyclic plan if, for every p ∈ Exec({f i }), either p reaches G or there exists some p ′ ∈ Exec({f i }) that extends p (i.e., p is a prefix of p ′ ) and reaches G. 1We assume that AP is a fixed set of atomic propositions.Transition Systems. As the basic system model, we use finite-state transition systems (TSs), which are tuples T = (L, l init , D, κ, ℓ) where L is a finite set of locations (we use "locations" to distinguish them from the "states" in a planning domain), l init ∈ L is an initial location, D is a finite set of directions, κ : L × D → L is the transition function, and ℓ : L → 2 AP labels each location with an evaluation of the APs. We use explicit directions in order to uniquely identify successor locations; we can easily model a traditional transition function κ : L → 2 L \ {∅} using directions. A path in T is an infinite sequence p ∈ L ω such that p(0) = l init , and for every k ∈ N, there exists some d ∈ D s.t. p(k + 1) = κ(p(k), d). We define Paths(T ) ⊆ L ω as the set of all paths in T .HyperLTL. As the basic specification language for hyperproperties, we use HyperLTL, an extension of LTL with explicit quantification over (execution) paths (Clarkson et al. 2014) . Let V = {π, π ′ , . . .} be a set of path variables. Hy-perLTL formulas are generated by the following grammarψ := a π | ψ ∧ ψ | ¬ψ | ψ U ψ | X ψ φ := Qπ. φ | ψwhere a ∈ AP , π ∈ V, and Q ∈ {∀, ∃}. We use the usual derived boolean and temporal constants and operators true, false, ∨, →, ↔, F ψ := true U ψ, G ψ := ¬ F ¬ψ.Given a TS T = (L, l init , D, κ, ℓ), we evaluate a Hyper-LTL formula in the context of a path assignment Π : V ⇀ L ω (mapping path variables to paths) as follows:Π, i |= T a π iff a ∈ ℓ Π(π)(i) Π, i |= T ψ 1 ∧ ψ 2 iff Π, i |= T ψ 1 and Π, i |= T ψ 2 Π, i |= T ¬ψ iff Π, i ̸ |= T ψ Π, i |= T X ψ iff Π, i + 1 |= T ψ Π, i |= T ψ 1 U ψ 2 iff ∃j ≥ i. Π, j |= T ψ 2 and ∀i ≤ k < j. Π, k |= T ψ 1 Π, i |= T Qπ. φ iff Qp ∈ Paths(T ). Π[π → p], i |= T φThe atomic formula a π holds whenever a holds in the current position i on the path bound to π (as given by ℓ). Boolean and temporal operators are evaluated as expected by updating the current evaluation position i, and quantification adds paths to Π. We refer to Finkbeiner (2023) for details. We say T satisfies φ, written T |= φ, if {}, 0 |= T φ, where {} denotes the path assignment with empty domain. 
verification via planning: 
 We want to automatically verify that T |= φ. To this end, we present a novel encoding into a planning problem, thus leveraging the extensive research and tool development within the planning community. As already outlined in Section 2, our main idea is to interpret existential quantification in φ as being resolved by an agent that picks transitions in T to construct a path. Throughout this section, we assume that T = (L, l init , D, κ, ℓ) is the fixed TS and φ = Q 1 π 1 . . . Q n π n . ψ the fixed HyperLTL formula over path variables π 1 , . . . , π n .DFAs and Reachability Specifications. A deterministic finite automaton (DFA) over some alphabet Σ is a tuple A = (Q, q 0 , ϱ, F ) where Q is a finite set of states, q 0 ∈ Q is an initial state, ϱ : Q × Σ → Q is a deterministic transition function, and F ⊆ Q is a set of accepting states. An infinite word u ∈ Σ ω is accepted by A if the unique run eventually reaches some state in F . We say φ is a Reachability Hyper-LTL formula if ψ (the LTL-like body of φ) is recognized by a DFA, i.e., some DFA A ψ = (Q ψ , q 0,ψ , ϱ ψ , F ψ ) over alphabet 2 AP×{π1,...,πn} accepts exactly those infinite words that satisfy ψ (recall that the atoms in the LTL-like formula ψ have the form a πi ∈ AP × {π 1 , . . . , π n }).We write V ∃ = {π i | Q i = ∃} for existentially quantified path variables in φ, and V ∀ for universally quantified ones.Definition 2. Define G reach T ,φ := (I, S, S 0 , {A i }, δ, {Ω i }, {ω i }, G) where I := {i | π i ∈ V ∃ }; S := {⟨l 1 , . . . , l n , q⟩ | q ∈ Q ψ ∧ ∀j. l j ∈ L};and S 0 := {⟨l init , . . . , l init , q 0,ψ ⟩}. For each i ∈ I, we set A i := D and define the transitions byδ(⟨l 1 , . . . , l n , q⟩, ({d j } πj ∈V ∃ )) := ⟨κ(l 1 , d 1 ), . . . , κ(l n , d n ), q ′ ⟩ | ∀π j ∈ V ∀ . d j ∈ D ∧ q ′ = ϱ ψ (q, n j=1 {(a, π j ) | a ∈ ℓ(l j )} , Ω i := {⟨l 1 , . . . , l i ⟩ | ∀j ≤ i. l j ∈ L}; ω i (⟨l 1 , . . . , l n , q⟩) := ⟨l 1 , . . . , l i ⟩; and G := {⟨l 1 , . . . , l n , q⟩ | q ∈ F ψ }.Let us step through this definition step-by-step. As already hinted in Section 2, we add one agent i for each existentially qualified path π i ∈ V ∃ . Each state has the form ⟨l 1 , . . . , l n , q⟩ and tracks a current location for each of the paths (where l j ∈ L is the current location for path π j ), and q tracks the current state of A ψ . Intuitively, the planning problem simulates π 1 , . . . , π n by keeping track of their current location (l 1 , . . . , l n ), and letting the actions chosen by the agents (for existentially quantified paths) or the nondeterminism (for universally quantified paths) fix the next location. We start each π j in the initial location l init and start the run of A ψ in the initial state q 0,ψ . The actions of each agent then directly correspond to directions in T . When given a joint action {d j } πj ∈V ∃ (i.e., a direction for each existentially quantified path), the transition formula considers all possible directions for universally quantified paths and updates each location l j based on the direction d j . Existentially quantified paths thus follow the direction selected by the respective agent, and universally quantified ones follow a non-deterministically chosen direction. In each step, we also update the state of A ψ : For each 1 ≤ j ≤ n, we collect all APs that hold in the current location ℓ(l j ) and index them with π j , thus obtaining a letter in 2 AP×{π1,...,πn} which we feed to the transition function of A ψ . As argued in Section 2, each agent i controlling π i ∈ V ∃ may only observe the traces π 1 , . . . , π i quantified before π i , so the observation set Ω i of agent i consist exactly of states of the form ⟨l 1 , . . . , l i ⟩ and the observation function ω i projects each state to the observable locations. Lastly, the goal consists of all states in which the automaton has reached one of A ψ 's accepting states.Theorem 1. Assume φ is a reachability HyperLTL formula. If G reach T ,φ admits a strong plan, then T |= φ. Proof Sketch. We can use the policies in a strong plan for G reach T ,φ to construct Skolem functions for existentially quantified paths in φ. The full proof is complex and provided in the supplementary materials.Factored Representation. In Definition 2, we used an explicit-state (flat) representation of the problem with |L| n * |Q ψ | states. In practice, many planning formats (e.g., STRIPS, PDDL, SAS) allow for a factored description of the state space, using roughly n • |L| + |Q ψ | many fluents that track the current location of each path individually. The possibility of using a factored representation is a core motivation for using planning tools for HyperLTL verification. In Section 7, we will show that this factored representation also leads to performance improvements over the SOTA.In the construction above, we assumed the φ denotes a reachability property. We can also handle the case in which φ denotes a safety HyperLTL formula, i.e., ψ expresses that "something bad may never happen". In the safety case, we again model ψ as a DFA A ψ = (Q ψ , q 0,ψ , ϱ ψ , F ψ ), but now say that an infinite word is accepted if it never visits a state in F ψ . As an example, (NI) is a safety HyperLTL formula.Different from reachability properties, safety properties reason about infinite executions (and not only finite prefixes thereof), so phasing it as a planning problem requires modifications. First, we add special sink states s win and s lose , and mark s win as the unique goal state. From any state ⟨l 1 , . . . , l n , q⟩ where q ∈ F ψ , we then deterministically move to s lose . Conversely, from any state ⟨l 1 , . . . , l n , q⟩ where q ̸ ∈ F ψ , we extend the transitions in Definition 2 with an additional non-deterministic transition to s win . The agents can thus never ensure a visit to s win , but a strong cyclic plan guarantees that we never visit a state in F ψ . We denote the resulting QDec-POMPD with G safe T ,φ ; a full description can be found in the supplementary materials. Theorem 2. Assume φ is a safety HyperLTL property. If G safe T ,φ admits a strong cyclic plan, then T |= φ. Full HyperLTL. Our construction can also be extended to handle full HyperLTL by reducing to planning problems with temporal goals specified in LTL(f) (Patrizi et al. 2011; Camacho et al. 2017; Camacho and McIlraith 2019) . We restrict our constriction to the case of reachability and safety properties as (1) this suffices for almost all properties of interest, and (2) it allows us to employ automated planners that yield strong (cyclic) plans for non-temporal objectives.In general, our encoding yields a planning problem that combines multiple agents, non-determinism, and partial observations. In many situations, however, the resulting problem does not require all these features: (1) For ∃ * properties, the planning problem is classical, i.e., consists of a single agent, deterministic actions, and full information. (2)  
implementation and experiments: 
 We have implemented our encoding for ∀ * ∃ * HyperLTL formulas in a prototype called HyPlan. Our tool produces FOND planning instance in an extension of PDDL, featuring (oneof p1 ... pn) expressions in action effects; A format widely supported by many FOND planners. We compare HyPlan against the parity-game (PG) based encoding for ∀ * ∃ * properties (Beutner and Finkbeiner 2022) . For our experiments, we collect the 10 NuSMV models from Hsu, Sánchez, and Bonakdarpour (2021) and generate random formulas of the form ∃π. ∃π ′ . F ψ and ∀π. ∃π ′ . G ψ where ψ is a temporal-operator-free formula. As remarked in Section 6.3, for the ∃∃ properties HyPlan produces classical planning problems (which we solve using Scorpion (Seipp and Helmert 2018)), whereas the ∀∃ properties yield FOND planning problems (which we solve using the FOND planner MyND (Mattmüller et al. 2010) ). We report the average size of the PG and PDDL planning problem, as well as the time taken for the ∃∃ and ∀∃ properties in Table 1 . As remarked in Section 3, the size of the PG is exponential, whereas the PDDL description is small and leaves the exact exploration strategy to the planner. Consequently, we observe that an existing (off-the-shelf) solver easily outperforms the game-based approach. 
conclusion: 
 We have presented a novel application of non-deterministic planning: the verification of hyperproperties. Our encoding is applicable to formulas with arbitrary quantifier prefixes (beyond ∀ * ∃ * ) and often yields classical or FOND planning instances that can be handled by existing mature planners. Our preliminary experiments show that off-the-shelf planners constitute an efficient verification method that outperforms existing game-based approaches. Moreover, any further progress into the development of non-deterministic planners (for which our work provides even more incentive) will directly improve our verification pipeline. 
 
 Appendix: A strong cyclic plan is one that always preserves the possibility of reaching the goal, i.e., at every point, the non-determinism can be resolved favorably such that the goal is reached. Our definition expresses exactly this: either p already reaches G or some extension of p can reach the goal. This definition is equivalent to the one ofCimatti et al. (2003). 


Decision: The reviewers agree that the paper presents an interesting contribution, relevant to ICAPS, and overall of good quality. Some minor issues were raised, which appear to be easily addressable in the final version, if the paper is accepted. In particular, I recommend the authors to cover also the additional related work mentioned by in the reviews. Additional suggestions are intended for a future extended version of the work, but the authors may try and account for some of them briefly in the present submission, such as the comparison with model checking.

Reviews: review: strength_weakness: strength_weakness: Two aspects of the document seem particularly weak. First, the state of the art is well covered, but a thorough comparison with model checking approaches is necessary to convince the reader of the effectiveness of the approach. Second, experiments have been shown in the paper (which is remarkable, given that it's a short paper), but no comparison has been made with other algorithms. In comparison to [1], the extension of the experimental section is too small to evaluate the approach against other algorithms and the behaviour of the translation-based approach for different types of formulae. I trust that the authors will do this in their future work.

What the Related work is missing, is probably "AutoHyper: Explicit-State Model Checking for HyperLTL", Raven Beutner and Bernd Finkbeiner, TACAS, Lecture Notes in Computer Science, 145-163 (2023), where the authors evaluate hyperproperties by applying language inclusion checks instead of explicit automaton complementation, and that can apply to arbitrary HyperLTL formulae as well as the current paper's approach.

Overall a good "Preliminary Work" short paper for ICAPS. We are waiting for a more complete paper.

[1] Tzu-Han, Hsu., C'esar, S'anchez., Sarai, Sheinvald., Borzoo, Bonakdarpour. (2023). Efficient Loop Conditions for Bounded Model Checking Hyperproperties.  66-84. doi: 10.48550/arXiv.2301.06209

# Minor considerations
- Sec.1 It is not clear what form has the output o in the example (it's a plan?)
- Def. 1 For each i \in I -> for each i \in I
- Sec. 6 I prefer the term "LTL fragment" rather than "LTL-like body" for a formula
- Sec. 6 I would rather incluse the alphabet Sigma in the definition of A, i.e. A = (Q, q0, rho, F, Sigma).
- Def. 2 The "forall j" of l_j \in L is not necessary
- Def. 2 Better to specify that j\in [1,n] when writing d_j \in D.
- It would be helpful for the reader to include an example of a formula in order to illustrate a TS.
questions: questions: 1) Is the DFA of section 6 a Büchi automaton? Looks like one.
2) In sec. 6.1, it's not clear how the non-determinism is treated. Does the planner selects a single outcome or does it progresses the state in a belief state (a set of possible destination states), keeping track of the whole uncertainty gained by the non-deterministic action? If a single outcome is selected, how this is done? My understanding is that, even if we're in a FOND, doing model-checking requires checking all the outcomes, i.e. a strong plan in Cimatti's sense.
3) I understand that formulae for checking deadlocks (as in invalid end states), correctness of system invariants, unreachability code,  and liveness properties through non-progress cycles (livelocks) are considered by the authors. What kind of expressvity do you expect from the QDec-POMDP translation?
strength_weakness: strength_weakness: I see no weakness in the paper, but I do have some minor comments and points for consideration, as follows.

# Minor Comments and Points of Consideration:

C1. Does OD stand for Observational Determinism? Please, state that as you do for NI (Non-Inference).

C2. To some extent, your definition of a strong cyclic plan (Footnote 1) takes into account fairness, right? Please, clarify that.

C3. What does $L^{\omega}$ mean? Is that the set of possible paths?! Please, clarify that.

C4. In the Proof Sketch of Theorem 1, you say: "We can use the policies of a strong plan ...". Shouldn't it be "We can use the paths of a strong plan ...". Please, clarify that.

C5. SOTA stands for state-of-the-art, right?! Please, state that.

C6. You could extend your construction and representation to support full HyperLTL with temporally extended goals expressed in LTL(f) using FOND4LTLf (https://github.com/whitemech/FOND4LTLf).
That would be a nice extension and addition as future work for HyPlan.

# Writing Issues and Typos:

W1. "The agent’s object ..." -> "The agent’s objective ...".
W2. "We restrict our constriction" -> "construction"?!
questions: questions: Please, address the following question in your response/rebuttal.

Q1. Why have you chosen to use MyND for non-deterministic planning? 
Is that because MyND can extract both strong and strong-cyclic plans? 
Is that because MyND can support both FOND and POND?
strength_weakness: strength_weakness: 1. This paper is not well organized. I think the author should place the related work in the Introduction and place the details of hyperproperty and HyperLTL in the following section.
2. This paper lacks an example about encoding a HyperLTL formula into a planning problem. 

Minor issues:
1.	In Introduction, “non-inference(NI)” => “non-interference(NI)”.
2.	In Section 6, “the fixed HyperLTL” => “is the fixed HyperLTL”
questions: questions: 1. Can any hyperproperty verification problem instance be reduced to a planning problem instance?
2. Is there a hyperproperty in your experiment that cannot be verified successfully? If it exists, what is the reason for it?