Fundamenta Informaticae - Volume 66, issue 3

Authors: Borzyszkowski, Tomasz

Article Type: Research Article

Abstract: We consider the Craig Interpolation Property for many sorted first-order logic. The Craig Interpolation Property explored in this paper is inspired by the institution independent generalization of this property presented in [21]. In [3] the author presents the interpolation result for the institution of many sorted first-order logic, with both morphisms in the pushout square being injective on sort names. The author also shows that the Craig Interpolation Property does not hold when both morphisms are …certain morphisms which are noninjective on sort names. An open question in that paper was whether the interpolation property holds with only one morphism being injective on sort names. In this paper we give answer to this question. Following the overall structure of the classical proof presented in [7] for single sorted first-order logic, but with new technicalities concerning the many sorted case, we show that many sorted first-order logic has the interpolation property when just one (left or right) morphism is injective on sort names. Show more

Keywords: Formal languages, Formal semantics, Specification languages, specifications, Interpolation property

Citation: Fundamenta Informaticae, vol. 66, no. 3, pp. 199-219, 2005

Authors: Devillers, Raymond | Klaudel, Hanna

Article Type: Research Article

Abstract: In the domain of parameterized composable high-level Petri nets (M-nets), we shall combine the refinement, the synchronization and the asynchronous link operations in a unified and general setup, while keeping the expected properties of those operations. In particular, the various high-level net operations are consistent through unfolding with their low-level counterparts, and the usual commutativity and idempotency properties are fulfilled at the syntactic level up to structural equivalences.

Keywords: High-level Petri nets, refinement, synchronization, asynchronous links, algebra

Citation: Fundamenta Informaticae, vol. 66, no. 3, pp. 221-257, 2005

Authors: Doberkat, Ernst-Erich

Article Type: Research Article

Abstract: We investigate similarities between non-deterministic and probabilistic ways of describing a system in terms of computation trees. We show that the construction of traces for both kinds of relations follows the same principles of construction. Representations of measurable trees in terms of probabilistic relations are given. This shows that stochastic relations may serve as refinements of their non-deterministic counterparts. A convexity argument formalizes the observation that non-deterministic system descriptions are underspecified when …compared to probabilistic ones. The mathematical tools come essentially from the theory of measurable selections. Show more

Keywords: Probabilistic relations, specification techniques (nondeterministic, stochastic), representation theory

Citation: Fundamenta Informaticae, vol. 66, no. 3, pp. 259-275, 2005

Authors: Finkel, Olivier

Article Type: Research Article

Abstract: In a recent paper [19, 20] Serre has presented some decidable winning conditions Ω _{A_1▹…▹A_n▹A_{n+1}} of arbitrarily high finite Borel complexity for games on finite graphs or on pushdown graphs. We answer in this paper several questions which were raised by Serre in [19,20]. We study classes C_n (A), defined in [20], and show that these classes are included in the class of non-ambiguous context free ω-languages. Moreover from …the study of a larger class C_n^λ (A) we infer that the complements of languages in C_n (A) are also non-ambiguous context free ω-languages. We conclude the study of classes C_n (A) by showing that they are neither closed under union nor under intersection. We prove also that there exists pushdown games, equipped with winning conditions in the form Ω_{A_1▹A_2} , where the winning sets are not deterministic context free languages, giving examples of winning sets which are non-deterministic non-ambiguous context free languages, inherently ambiguous context free languages, or even non context free languages. Show more

Keywords: Pushdown automata, infinite two-player games, pushdown games, winning conditions, Borel complexity, context free ω-languages, closure under boolean operations, set of winning positions

Citation: Fundamenta Informaticae, vol. 66, no. 3, pp. 277-298, 2005

Authors: Moshkova, Albina

Article Type: Research Article

Abstract: In the paper so-called retaining faults of combinatorial circuits are considered. It is proved that for iteration-free circuits there exist decision trees which solve the problem of circuit diagnosis relatively retaining faults and which depth is bounded from above by a linear function on the number of gates in circuits. For each closed class of Boolean functions a basis is found which is optimal from the point of view of complexity of diagnosis of formula-like circuits …over this basis (during the procedure of diagnosis each formula-like circuit is transformed into an iteration-free circuit). Relationships are studied between two types of Shannon functions. A function of the first type characterizes the complexity of diagnosis of formula-like circuits realizing Boolean functions from a closed class. A function of the second type characterizes the complexity of formulas realizing Boolean functions from a closed class. The obtained relationships allowe to transfer some known results for Shannon functions of the second type on the case of Shannon functions of the first type. Show more

Keywords: combinatorial circuits, retaining faults, diagnosis, decision trees

Citation: Fundamenta Informaticae, vol. 66, no. 3, pp. 299-313, 2005