Consider the following specification technique.A specification consists of a finite set of triples $\langle C, A, C' \rangle$,where $A$ is the name of an action and $C, C'$ are conditions, that is,propositional formulas over propositional variables.Example rules (in a more suggestive notation):$C_1 \wedge \neg(C_2 \vee C_3) \stackrel{A_1}{\longrightarrow} C_1 \wedge \neg C_2$$C_1 \vee C_3 \stackrel{A_2}{\longrightarrow} C_2 \vee C_3$Each triple specifies an event together with its preconditions and postconditions:the semantics can be defined by saying that the system being described has a state space consisting of the set of possible truth value assignments to the propositional variables, and that the actions may take the system from any state in which the precondition of a rule for that action holds to any state in which the postcondition of that same rule holds.This formalism, or a restriction (e.g. no negation in formulas, or only Horn clauses) will only suit my purposes if software exists that can answer questions such asGiven a condition, which events may happen?Given a condition, may it lead to deadlock (a condition in which no event can happen)?Given a condition, will it never lead to deadlock?Do deadlock conditions exist at all?Given a condition, which events can never happen?in under a second.My question: what to Google for?Does this formalism have a name?Can it be converted to one for which equivalent problems have been studied?I'm thinking of safe Petri nets, for which I've found some papers, Hoare logic, dynamic logic, no doubt there is more.Does such software exist?  How do I Google for it?
Spot the formalism (some kind of process logic)
logic;model checking;linear temporal logic;hoare logic