Guarded logic

A guarded logical choice is one where any change in true affects all decisions made down the line.

Both terms found sub-classes of first-class logic and efficiently used in solvable languages which can be used for research.

Later Moshe Y. Vardi[3] made a conjecture that a tree model would work for many modal style logics.

It was found that the robust decidability of guarded logic could be generalized with a tree model property.

It also so happens that invariance under bisimulation is the root of tree model property which helps towards defining automata theory.

[4] Let B be a relational structure with universe B and vocabulary τ. i) A set X ⊆ B is guarded in B if there exists a ground atom α(b_1, ..., b_k) in B such that X = {b_1, ..., b_k}.

[5] A guarded bisimulation between two τ-structures A and B is a non-empty set I of finite partial isomorphic f: X → Y from A to B such that the back and forth conditions are satisfied.