A Logic Based Approach to the Static Analysis of Production Systems

In this paper we present an embedding of propositional production systems into µ-calculus, and first-order production systems into fixed-point logic, with the aim of using these logics for the static analysis of production systems with varying working memories. We encode properties such as termination and confluence in these logics, and briefly discuss which ones cannot be expressed, depending on the expressivity of the logic. We show how the embeddings can be used for reasoning over the production system, and use known results to obtain upper bounds for special cases. The strong correspondence between the structure of the models of the encodings and the runs of the production systems enables the straightforward modeling of properties of the system in the logic.

• Type: Conference
• Year: 2009
• Where: RR
• Authors: Jos de Bruijn, Martín Rezk
• Keywords: Internet Technology, Production Systems, Propositional Production Systems, RR 2009, first-order Production Systems