International Journal of Foundations of Computer Science

Conjecture 11 of [Lagoutte, Maletti: Survey — Weighted extended top-down tree transducers — Part III: Composition. Proc. AFCS, LNCS 7020, p. 272–308, Springer 2011] is confirmed. It is demonstrated that the composition of a constant weighted extended tree transducer with a linear weighted top-down tree transducer can be computed by a single weighted extended tree transducer. Whereas linearity and the top-down property are syntactic, the constant property is semantic. The decidability of the constant property is investigated in several restricted settings.

In this paper, we propose a logic-based characterization of uncertainty in architectures of parametric component-based systems, where the parameter is the number of instances of each component type. For this, we firstly introduce an extended propositional interaction logic over De Morgan algebras and we show that its formulas can encode the uncertainty of several architectures applied in systems with a finite number of components. In turn, we introduce a first-order extended interaction logic over De Morgan algebras which is applied for modelling uncertainty in the interactions of well-known parametric architectures. Moreover, we prove that the equivalence problem for a large class of formulas of that logic is decidable in doubly exponential time by providing an effective translation to fuzzy recognizable series. For any such formula over a totally ordered De Morgan algebra, we further prove that we can compute in exponential time the set of sequences of parametric fuzzy interactions which ensure the trustworthiness of the formula according to a particular threshold.

We introduce and investigate a weighted propositional configuration logic over De Morgan algebras. This logic is able to describe software architectures with quantitative features especially the uncertainty of the interactions that occur in the architecture. We deal with the equivalence problem of formulas in our logic by showing that every formula can be written in a specific form. Surprisingly, there are formulas which are equivalent only over specific De Morgan algebras. We provide examples of formulas in our logic which describe well-known software architectures equipped with quantitative features such as the uncertainty and reliability of their interactions.

A weighted finite automaton has the finite-image property if the image of the weighted language associated with it is finite. We show two undecidability results concerning the finite-image property of weighted finite automata over semirings, respectively strong bimonoids. Firstly, we give a computable idempotent commutative past-finite ordered semiring such that it is undecidable, for an arbitrary deterministic weighted finite automaton ${𝒜}$ over that semiring, whether ${𝒜}$ has the finite-image property. Secondly, we give a computable commutative past-finite monotonic ordered strong bimonoid such that it is undecidable, for an arbitrary weighted finite automaton ${𝒜}$ over that strong bimonoid, whether ${𝒜}$ has the finite-image property. This shows that recent decidability results for suitable weighted finite automata over past-finite monotonic strong bimonoids cannot be extended to natural classes of ordered semirings and ordered strong bimonoids without further assumptions.

A deterministic finite automaton in which every non-empty set of states occurs as the image of the whole state set under the action of a suitable input word is called completely reachable. We characterize such automata in terms of graphs and trees.