IteratedConditionSystems.hpp File Reference

Plans for satisfaction problems given by transition functions. More...

Go to the source code of this file.

Detailed Description

Plans for satisfaction problems given by transition functions.

Basic notions
  • Given a set V of variables and a (uniform) domain D of values; yielding the set TASS(V,D) of all total assignments f: V -> D.
  • An "iterated condition system" (ics) is specified by three conditions (see 'The notion of "condition"' in ComputerAlgebra/Satisfiability/Lisp/plans/SatisfactionProblems.hpp):
    1. The initial condition S(f).
    2. The transition condition T(f,g).
    3. An invariant I(f).
  • Given an ics (V,D,S,T,I), for k in NN_0 the set R_k of total assignments reachable in k steps is defined by induction as follows:
    1. R_0 is the set of f with S(f) and I(f).
    2. R_{k+1} is the set of g such that f in R_k exists, and we have T(f,g) and I(g).
  • The task is, for a given condition C to find k in NN_0 and f in R_k with not C(f). Call it a "falsifying solution".
  • If no "falsifying solution" exists (for the given C), then C is called "valid" for the ics.
  • Typically one also wants (f_0, ..., f_k), f_k = f, the "trace", witnessing f in R_k, that is,
    1. S(f_0),
    2. for all i < k we have T(f_i,f_{i+1}) and I(f_i),
    3. and finally we have I(f_k) and not C(f_k).
  • Additionally typically one wants the smallest such k, that is, for i < k we C(f_i).
Finding literature
  • The above notion of an "ics" is likely rather common.
  • We need literature.
The trivial algorithm
  • Given an ics (V,D,S,T,I) and the target condition C, the trivial algorithm is to compute R_0, R_1, ..., until either we find a k such that R_k contains an element fulfilling not C, or we finally find k and k' < k such that R_k = R_{k'}, in which case C is valid for the ics.
  • There should exist some complexity result on solving ics showing that "in general" this is the best what can be done.
AES as an ics
Applications from railway safety
  • Discuss with PJ and Markus Roggenbach potential collaborations.

Definition in file IteratedConditionSystems.hpp.