SUCCINCT-REACH, reachability in a succinct transition system
Lax134656.SuccinctReach · concepts/Lax134656/SuccinctReach.lean · lax-134656
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
An instance describes a transition system succinctly. Some of its elements are state variables, each with next-state copies given by a binary relation, and its clauses, with positive and negative occurrences of variables, are split into three groups: transition, source and target clauses. A state of the system is a truth assignment to the state variables. There is a transition from a state to a state when some valuation of all the variables satisfies every transition clause, agrees with on the state variables and gives each next-state copy the value gives to its variable; a state is a source, respectively a target, when some valuation agreeing with it on the state variables satisfies every source, respectively target, clause.
An instance is a yes-instance of SUCCINCT-REACH when some target state is reachable from some source state by a possibly empty sequence of transitions; the problem is the decision problem of the structures isomorphic to such an instance. The system has exponentially many states in the size of its description.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.ModelTheory.Semantics |
| 2 | import Mathlib.Logic.Relation |
| 3 | import Lax904597.Problems |
| 4 | import Lax485149.Problems |
| 5 | |
| 6 | /-! |
| 7 | --- |
| 8 | title: SUCCINCT-REACH, reachability in a succinct transition system |
| 9 | type: definition |
| 10 | --- |
| 11 | An instance describes a transition system succinctly. Some of its elements |
| 12 | are state variables, each with next-state copies given by a binary |
| 13 | relation, and its clauses, with positive and negative occurrences of |
| 14 | variables, are split into three groups: transition, source and target |
| 15 | clauses. A state of the system is a truth assignment to the state |
| 16 | variables. There is a transition from a state to a state when some |
| 17 | valuation of all the variables satisfies every transition clause, agrees |
| 18 | with on the state variables and gives each next-state copy the value |
| 19 | gives to its variable; a state is a source, respectively a target, |
| 20 | when some valuation agreeing with it on the state variables satisfies every |
| 21 | source, respectively target, clause. |
| 22 | |
| 23 | An instance is a yes-instance of SUCCINCT-REACH when some target state is |
| 24 | reachable from some source state by a possibly empty sequence of |
| 25 | transitions; the problem is the decision problem of the structures |
| 26 | isomorphic to such an instance. The system has exponentially many states in |
| 27 | the size of its description. |
| 28 | -/ |
| 29 | |
| 30 | namespace Lax134656.SuccinctReach |
| 31 | |
| 32 | open Lax904597.Problems Lax485149.Problems |
| 33 | |
| 34 | open FirstOrder |
| 35 | |
| 36 | open FirstOrder.Language |
| 37 | |
| 38 | /-- The relation symbols of the language. -/ |
| 39 | inductive transSysRel : ℕ → Type where |
| 40 | /-- `stateVar x`: the element `x` is a state variable. -/ |
| 41 | | stateVar : transSysRel 1 |
| 42 | /-- `next x y`: the element `y` is the next-state copy of the state |
| 43 | variable `x`. -/ |
| 44 | | next : transSysRel 2 |
| 45 | /-- `stepCl c`: the element `c` is a clause of the transition formula. -/ |
| 46 | | stepCl : transSysRel 1 |
| 47 | /-- `srcCl c`: the element `c` is a clause of the source formula. -/ |
| 48 | | srcCl : transSysRel 1 |
| 49 | /-- `tgtCl c`: the element `c` is a clause of the target formula. -/ |
| 50 | | tgtCl : transSysRel 1 |
| 51 | /-- `posIn c x`: the variable `x` occurs positively in the clause `c`. -/ |
| 52 | | posIn : transSysRel 2 |
| 53 | /-- `negIn c x`: the variable `x` occurs negatively in the clause `c`. -/ |
| 54 | | negIn : transSysRel 2 |
| 55 | deriving DecidableEq |
| 56 | |
| 57 | /-- The relational vocabulary of succinctly described transition systems: the |
| 58 | state variables and their next-state copies, three groups of clauses, and the |
| 59 | two literal-occurrence predicates of CNF instances. -/ |
| 60 | def transSys : FirstOrder.Language := |
| 61 | ⟨fun _ => Empty, transSysRel⟩ |
| 62 | |
| 63 | instance instIsRelationalTransSys : FirstOrder.Language.IsRelational transSys := fun _ => |
| 64 | (inferInstance : IsEmpty Empty) |
| 65 | |
| 66 | /-- `stateVar x`: the element `x` is a state variable. -/ |
| 67 | abbrev tsStateVar : transSys.Relations 1 := |
| 68 | .stateVar |
| 69 | |
| 70 | /-- `next x y`: the element `y` is the next-state copy of the state |
| 71 | variable `x`. -/ |
| 72 | abbrev tsNext : transSys.Relations 2 := |
| 73 | .next |
| 74 | |
| 75 | /-- `stepCl c`: the element `c` is a clause of the transition formula. -/ |
| 76 | abbrev tsStepCl : transSys.Relations 1 := |
| 77 | .stepCl |
| 78 | |
| 79 | /-- `srcCl c`: the element `c` is a clause of the source formula. -/ |
| 80 | abbrev tsSrcCl : transSys.Relations 1 := |
| 81 | .srcCl |
| 82 | |
| 83 | /-- `tgtCl c`: the element `c` is a clause of the target formula. -/ |
| 84 | abbrev tsTgtCl : transSys.Relations 1 := |
| 85 | .tgtCl |
| 86 | |
| 87 | /-- `posIn c x`: the variable `x` occurs positively in the clause `c`. -/ |
| 88 | abbrev tsPosIn : transSys.Relations 2 := |
| 89 | .posIn |
| 90 | |
| 91 | /-- `negIn c x`: the variable `x` occurs negatively in the clause `c`. -/ |
| 92 | abbrev tsNegIn : transSys.Relations 2 := |
| 93 | .negIn |
| 94 | |
| 95 | open FirstOrder |
| 96 | |
| 97 | open Language Structure |
| 98 | |
| 99 | section Semantics |
| 100 | |
| 101 | variable (A : Type) [transSys.Structure A] |
| 102 | |
| 103 | /-- A valuation satisfies a group of clauses when every clause of the group |
| 104 | contains a literal it makes true. Elements that are not clauses of the group |
| 105 | impose nothing, exactly as for satisfiability. -/ |
| 106 | def ClausesHold (ν : A → Prop) (grp : transSys.Relations 1) : Prop := |
| 107 | ∀ c : A, RelMap grp ![c] → |
| 108 | ∃ x : A, (RelMap tsPosIn ![c, x] ∧ ν x) ∨ (RelMap tsNegIn ![c, x] ∧ ¬ν x) |
| 109 | |
| 110 | /-- The valuation `ν` *reads* the state `S`: on every state variable it agrees |
| 111 | with `S`. This is the only way a clause group sees the current state. -/ |
| 112 | def ReadsCur (ν : A → Prop) (S : A → Prop) : Prop := |
| 113 | ∀ x : A, RelMap tsStateVar ![x] → (ν x ↔ S x) |
| 114 | |
| 115 | /-- The valuation `ν` *writes* the state `S'`: on the next-state copy of every |
| 116 | state variable it holds exactly the value `S'` gives to that variable. -/ |
| 117 | def WritesNext (ν : A → Prop) (S' : A → Prop) : Prop := |
| 118 | ∀ x y : A, RelMap tsStateVar ![x] → RelMap tsNext ![x, y] → (ν y ↔ S' x) |
| 119 | |
| 120 | /-- One transition of the system: some valuation satisfies every transition |
| 121 | clause while reading `S` on the state variables and writing `S'` on their |
| 122 | next-state copies. The valuation is existentially quantified, so the auxiliary |
| 123 | variables of the transition formula are free to take whatever values the |
| 124 | clauses need. -/ |
| 125 | def StepRel (S S' : A → Prop) : Prop := |
| 126 | ∃ ν : A → Prop, ClausesHold A ν tsStepCl ∧ ReadsCur A ν S ∧ WritesNext A ν S' |
| 127 | |
| 128 | /-- A state is a source state when some valuation reading it satisfies every |
| 129 | clause of the source formula. -/ |
| 130 | def IsStart (S : A → Prop) : Prop := |
| 131 | ∃ ν : A → Prop, ClausesHold A ν tsSrcCl ∧ ReadsCur A ν S |
| 132 | |
| 133 | /-- A state is a target state when some valuation reading it satisfies every |
| 134 | clause of the target formula. -/ |
| 135 | def IsGoal (S : A → Prop) : Prop := |
| 136 | ∃ ν : A → Prop, ClausesHold A ν tsTgtCl ∧ ReadsCur A ν S |
| 137 | |
| 138 | /-- **The yes-instances of SUCCINCT-REACH**: some target state is reachable |
| 139 | from some source state along the transitions described by the clauses. -/ |
| 140 | def SuccinctReachable : Prop := |
| 141 | ∃ S S' : A → Prop, IsStart A S ∧ IsGoal A S' ∧ Relation.ReflTransGen (StepRel A) S S' |
| 142 | |
| 143 | end Semantics |
| 144 | |
| 145 | /-- SUCCINCT-REACH: is some target state reachable from some source state in |
| 146 | the succinctly described transition system? -/ |
| 147 | def SUCCINCTREACH : DecisionProblem transSys := |
| 148 | DecisionProblem.ofPred fun A _ => SuccinctReachable A |
| 149 | |
| 150 | end Lax134656.SuccinctReach |
| 151 |
Builds on
Used by
Lax134656.AbiteboulVianuLax134656.AbiteboulVianuOrderedLax134656.HierarchyInPSPACELax134656.InflationaryInPartialLax134656.PartialFixedPointCaptureLax134656.PartialFixedPointClosureLax134656.PSPACEClosureLax134656.PSPACEEqCoPSPACELax134656.QsatInvarianceLax134656.QsatPSPACECompleteLax134656.SpaceBoundedMachineInvarianceLax134656.SpaceMachinesPSPACECompleteLax134656.SuccinctReachInvarianceLax134656.SuccinctReachPSPACECompleteLax134656.TransitiveClosureWithoutOrder
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments