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.
 Todo:
 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):

The initial condition S(f).

The transition condition T(f,g).

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:

R_0 is the set of f with S(f) and I(f).

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,

S(f_0),

for all i < k we have T(f_i,f_{i+1}) and I(f_i),

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).
 Todo:
 Finding literature

The above notion of an "ics" is likely rather common.

We need literature.
 Todo:
 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.
 Todo:
 AES as an ics
 Todo:
 Applications from railway safety

Discuss with PJ and Markus Roggenbach potential collaborations.
Definition in file IteratedConditionSystems.hpp.