Using First-Order Logic to Reason about Submodule Construction

12 years 7 months ago
Using First-Order Logic to Reason about Submodule Construction
We consider the following problem: For a system consisting of two components, the behavior of one component is known as well as the desired global behavior. What should be the behavior of the second component such that the behavior of the composition of the two conforms to the desired behavior ? - This problem has been called "submodule construction" or "equation solving"; and in the context of supervisory control, it is the problem of designing a suitable controller (second component) which controls a given system to be controlled (first component). Solutions to this problem have been described in the context of various specification formalisms and various conformance relations. This paper presents a new formulation of this problem and its solution in first-order logic. It is also shown how the solutions for submodule construction in various specification formalisms can be derived from the solution in logic. The simple proof of correctness for the logic solution is...
Gregor von Bochmann
Added 17 Feb 2011
Updated 17 Feb 2011
Type Journal
Year 2009
Authors Gregor von Bochmann
Comments (0)