A Dynamic Logic for Configuration
Ching Hoo Tang, Christoph Weidenbach · Max Planck Digital Library · 2016
We define the new dynamic logic PIDL+ that extends our previously developed logic PIDL (Propositional Interactive Dynamic Logic) with arithmetic constraints.The language of PIDL+ is motivated by real world configuration systems, in particular, configuration systems for power plants.A PIDL+ specification consists of the description of an initial state, global constraints, and actions.Its semantics are the possible worlds starting from the initial state, spanned by the actions and restricted by the constraints.It distinguishes user actions from rule actions.Any user action is followed by a unique fixed point, called rule-terminal state, generated through exhaustive application of rule actions from the specification.The built in rule action fixpoint semantics and arithmetic constraints distinguish PIDL+ from known dynamic or action logics.Correctness of a PIDL+ specification as well as reachability of a particular state are decidable.We provide sound and complete algorithms.