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 as

  • Given 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?

  • $\begingroup$ The properties you are asking for a relatively simple and they do not require complex temporal formulas. Could you refine what ``under a second'' means. Is it under a second given a fresh specification, or the tool can take minutes to build an internal representation of the model and then respond to specific queries? $\endgroup$ – Dmitri Chubarov Oct 20 '12 at 6:35
  • $\begingroup$ Where did you find this? What happens to the propositions variables not specified in the post condition? $\endgroup$ – Dave Clarke Oct 20 '12 at 7:31
  • $\begingroup$ @Dmitri Chubarov: I'd like to use it while the specification is written, so it would be convenient if it can be done without preprocessing, but if need be, preprocessing will usually be fine (e.g. perhaps unfolding into a finite state machine may often be good enough). $\endgroup$ – reinierpost Oct 23 '12 at 8:39
  • $\begingroup$ @Dave Clarke: I found it at the back of my mind when I was considering what kind of formalism I'd need, and it's very similar to things I was taught in college (another is logical circuit design), but not quite the same. $\endgroup$ – reinierpost Oct 23 '12 at 8:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.