SUCCINCT-REACH: reachability in a propositionally described transition system

The vocabulary and semantics of the canonical PSPACE problem of this library: reachability in a graph whose vertices are the truth assignments to a set of state variables and whose edges, source set and target set are described by three CNF formulas rather than listed. The graph has exponentially many vertices in the size of the instance – it is succinctly represented – which is exactly why walking it costs polynomial space and not polynomial time.

Under other names the same problem is propositional STRIPS plan existence, and it is the reachability query at the heart of symbolic model checking.

The instance

An instance is a FirstOrder.Language.transSys-structure. Its elements are propositional variables and clauses at once, as in FirstOrder.Language.sat, with

• stateVar x: x is a state variable – a bit of the vertex being walked;
• next x y: y is the next-state copy of the state variable x, so that one clause set can talk about a state and its successor at once;
• stepCl c, srcCl c, tgtCl c: c is a clause of the transition, of the source or of the target formula;
• posIn c x, negIn c x: the variable x occurs positively (negatively) in the clause c, as for SAT.

Variables that are neither state variables nor next-state copies are auxiliary: they are quantified existentially inside each clause group, which is what lets a CNF describe an arbitrary transition relation (a Tseitin encoding introduces exactly such variables for its gates).

The semantics

A state is an arbitrary predicate on the universe; only its restriction to the state variables matters, since that is all the clause groups can read (DescriptiveComplexity.ReadsCur). There is a transition from S to S' when some assignment satisfies every transition clause while reading S on the state variables and writing S' on their next-state copies (DescriptiveComplexity.StepRel). The instance is a yes-instance when some target state is reachable from some source state (DescriptiveComplexity.SuccinctReachable).

This is the syntactic image of SO(TC), in the same sense that a CNF is the syntactic image of an existential second-order block: a state is a monadic relation variable, a transition is a first-order condition on two consecutive states, and reachability is the transitive closure. That is what makes the membership half cheap (DescriptiveComplexity.Problems.SuccinctReach.Membership) and the hardness half a Tseitin translation.

inductive FirstOrder.Language.transSysRel : ℕ → Type

Relation symbols of the language of propositionally described transition systems.

• stateVar : transSysRel 1

  stateVar x: the element x is a state variable.

• next : transSysRel 2

  next x y: the element y is the next-state copy of the state variable x.

• stepCl : transSysRel 1

  stepCl c: the element c is a clause of the transition formula.

• srcCl : transSysRel 1

  srcCl c: the element c is a clause of the source formula.

• tgtCl : transSysRel 1

  tgtCl c: the element c is a clause of the target formula.

• posIn : transSysRel 2

  posIn c x: the variable x occurs positively in the clause c.

• negIn : transSysRel 2

  negIn c x: the variable x occurs negatively in the clause c.

def FirstOrder.Language.instDecidableEqTransSysRel.decEq {a✝ : ℕ} (x✝ x✝¹ : transSysRel a✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqTransSysRel {a✝ : ℕ} : DecidableEq (transSysRel a✝)

Equations

• FirstOrder.Language.instDecidableEqTransSysRel = FirstOrder.Language.instDecidableEqTransSysRel.decEq

def FirstOrder.Language.transSys : Language

The relational vocabulary of succinctly described transition systems: the state variables and their next-state copies, three groups of clauses, and the two literal-occurrence predicates of FirstOrder.Language.sat.

Equations

• FirstOrder.Language.transSys = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.transSysRel }

instance FirstOrder.Language.instIsRelationalTransSys : Language.transSys.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.tsStateVar : Language.transSys.Relations 1

The symbol for “is a state variable”.

Equations

• FirstOrder.Language.tsStateVar = FirstOrder.Language.transSysRel.stateVar

@[reducible, inline]

abbrev FirstOrder.Language.tsNext : Language.transSys.Relations 2

The symbol for “is the next-state copy of”.

Equations

• FirstOrder.Language.tsNext = FirstOrder.Language.transSysRel.next

@[reducible, inline]

abbrev FirstOrder.Language.tsStepCl : Language.transSys.Relations 1

The symbol for “is a clause of the transition formula”.

Equations

• FirstOrder.Language.tsStepCl = FirstOrder.Language.transSysRel.stepCl

@[reducible, inline]

abbrev FirstOrder.Language.tsSrcCl : Language.transSys.Relations 1

The symbol for “is a clause of the source formula”.

Equations

• FirstOrder.Language.tsSrcCl = FirstOrder.Language.transSysRel.srcCl

@[reducible, inline]

abbrev FirstOrder.Language.tsTgtCl : Language.transSys.Relations 1

The symbol for “is a clause of the target formula”.

Equations

• FirstOrder.Language.tsTgtCl = FirstOrder.Language.transSysRel.tgtCl

@[reducible, inline]

abbrev FirstOrder.Language.tsPosIn : Language.transSys.Relations 2

The symbol for “occurs positively in”.

Equations

• FirstOrder.Language.tsPosIn = FirstOrder.Language.transSysRel.posIn

@[reducible, inline]

abbrev FirstOrder.Language.tsNegIn : Language.transSys.Relations 2

The symbol for “occurs negatively in”.

Equations

• FirstOrder.Language.tsNegIn = FirstOrder.Language.transSysRel.negIn

def DescriptiveComplexity.ClausesHold (A : Type) [FirstOrder.Language.transSys.Structure A] (ν : A → Prop) (grp : FirstOrder.Language.transSys.Relations 1) : Prop

A valuation satisfies a group of clauses when every clause of the group contains a literal it makes true. Elements that are not clauses of the group impose nothing, exactly as in DescriptiveComplexity.Satisfiable.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.ReadsCur (A : Type) [FirstOrder.Language.transSys.Structure A] (ν S : A → Prop) : Prop

The valuation ν reads the state S: on every state variable it agrees with S. This is the only way a clause group sees the current state.

Equations

• DescriptiveComplexity.ReadsCur A ν S = ∀ (x : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsStateVar ![x] → (ν x ↔ S x)

def DescriptiveComplexity.WritesNext (A : Type) [FirstOrder.Language.transSys.Structure A] (ν S' : A → Prop) : Prop

The valuation ν writes the state S': on the next-state copy of every state variable it holds exactly the value S' gives to that variable.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.StepRel (A : Type) [FirstOrder.Language.transSys.Structure A] (S S' : A → Prop) : Prop

One transition of the system: some valuation satisfies every transition clause while reading S on the state variables and writing S' on their next-state copies. The valuation is existentially quantified, so the auxiliary variables of the transition formula are free to take whatever values the clauses need.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.IsStart (A : Type) [FirstOrder.Language.transSys.Structure A] (S : A → Prop) : Prop

A state is a source state when some valuation reading it satisfies every clause of the source formula.

Equations

• DescriptiveComplexity.IsStart A S = ∃ (ν : A → Prop), DescriptiveComplexity.ClausesHold A ν FirstOrder.Language.tsSrcCl ∧ DescriptiveComplexity.ReadsCur A ν S

def DescriptiveComplexity.IsGoal (A : Type) [FirstOrder.Language.transSys.Structure A] (S : A → Prop) : Prop

A state is a target state when some valuation reading it satisfies every clause of the target formula.

Equations

• DescriptiveComplexity.IsGoal A S = ∃ (ν : A → Prop), DescriptiveComplexity.ClausesHold A ν FirstOrder.Language.tsTgtCl ∧ DescriptiveComplexity.ReadsCur A ν S

def DescriptiveComplexity.SuccinctReachable (A : Type) [FirstOrder.Language.transSys.Structure A] : Prop

The yes-instances of SUCCINCT-REACH: some target state is reachable from some source state along the transitions described by the clauses.

Equations

• One or more equations did not get rendered due to their size.

Isomorphism-invariance

Everything transports along the push-forward of a predicate through the isomorphism; each piece of the semantics is pushed in one direction only, and the equivalence comes from applying the result to the inverse isomorphism.

theorem DescriptiveComplexity.succinctReachable_iso {A B : Type} [FirstOrder.Language.transSys.Structure A] [FirstOrder.Language.transSys.Structure B] (e : FirstOrder.Language.transSys.Equiv A B) : SuccinctReachable A ↔ SuccinctReachable B

Reachability in a succinctly described transition system is isomorphism-invariant.

def DescriptiveComplexity.SUCCINCTREACH : DecisionProblem FirstOrder.Language.transSys

SUCCINCT-REACH, as a problem on FirstOrder.Language.transSys-structures: is some target state reachable from some source state in the transition system described by the three clause groups?

Equations

• DescriptiveComplexity.SUCCINCTREACH = { Holds := fun (A : Type) (inst : FirstOrder.Language.transSys.Structure A) => DescriptiveComplexity.SuccinctReachable A, iso_invariant := ⋯ }