Mathematical foundations for the reconfiguration paradigm

点击翻译按钮获取中文摘要

In the final year of the present project, we proved a Robinson Consistency Property for a large class of hybrid-dynamic logics. In classical first-order logic, Robinson's Consistency Theorem was a historical forerunner of Craig's celebrated Interpolation Theorem, to which it is equivalent. In the context of first-order logic, it is known since Lindstrom's work that in the presence of compactness, the Robinson Consistency Property is a consequence of the Omitting Types Theorem. Following in Lindstrom's footsteps, we used an Omitting Types Theorem for many-sorted hybrid-dynamic first-order logics established in the previous year of the present project to obtain a Robinson Consistency Theorem. An important corollary of this result is interpolation, which is a logical property that mostly deal with combining and decomposing theories. The reason for the interest in interpolation is the fact that it is the source of many other results. For structured specifications and formal methods, interpolation ensures a good compositional behavior of module semantics.Throughout the entire research period dedicated to the present project, we set the foundations for the formal specification and verification of reconfigurable systems. The knowledge on hybrid-dynamic logics -- recognized as suitable for describing and reasoning about systems with reconfigurable features -- was developed uniformly at an abstract level provided by the category-based definition of stratified institution.