Synthesis for Structure Rewriting Systems

Abstract. The description of a single state of a modelled system is often complex in practice, but few procedures for synthesis address this problem in depth. We study systems in which a state is described by an arbitrary finite structure, and changes of the state are represented by structure rewriting rules, a generalisation of term and graph rewriting. Both the environment and the controller are allowed to change the structure in this way, and the question we ask is how a strategy for the controller that ensures a given property can be synthesised. We focus on one particular class of structure rewriting rules, namely on separated structure rewriting, a limited syntactic class of rules. To counter this restrictiveness, we allow the property to be ensured by the controller to be specified in a very expressive logic: a combination of monadic second-order logic evaluated on states and the modal µ-calculus for the temporal evolution of the whole system. We show that for the considered ...

• Type: Conference
• Year: 2009
• Where: MFCS
• Authors: Lukasz Kaiser
• Keywords: Arbitrary finite Structure, Graph Rewriting, MFCS 2009, Structure Rewriting Rules, Theoretical Computer Science