Categorical abstract data type (CADT)
Categories of partial morphisms and the relation between type structures. Partial variations on a theme of Friedman and Statman
Characteristic formulae for timed automata
Characteristic Formulae for Timed Automata
This paper offers characteristic formula constructions in the real-time logic Lν for several behavioural relations between (states of) timed automata. The behavioural relations studied in this work are timed (bi)similarity, timed ready simulation, faster-than bisimilarity and timed trace inclusion. The characteristic formulae delivered by our constructions have size which is linear in that of the timed automaton they logically describe. This also applies to the characteristic formula for...
Characterizing the complexity of boolean functions represented by well-structured graph-driven parity-FBDDs
We investigate well-structured graph-driven parity-FBDDs, which strictly generalize the two well-known models parity OBDDs and well-structured graph-driven FBDDs. The first main result is a characterization of the complexity of Boolean functions represented by well-structured graph-driven parity-FBDDs in terms of invariants of the function represented and the graph-ordering used. As a consequence, we derive a lower bound criterion and prove an exponential lower bound for certain linear code functions....
Characterizing the Complexity of Boolean Functions represented by Well-Structured Graph-Driven Parity-FBDDs
We investigate well-structured graph-driven parity-FBDDs, which strictly generalize the two well-known models parity OBDDs and well-structured graph-driven FBDDs. The first main result is a characterization of the complexity of Boolean functions represented by well-structured graph-driven parity-FBDDs in terms of invariants of the function represented and the graph-ordering used. As a consequence, we derive a lower bound criterion and prove an exponential lower bound for certain linear code functions. The...
Comparaison et équivalence de sémantiques pour les schémas de programmes non déterministes
Correctness of horizontal and vertical composition for implementation concepts based on constructors and abstractors.
A new implementation concept for parameterized specifications based on constructors and abstractors was recently introduced by Orejas, Navarro and Sánchez which includes most of the implementation concepts in the literature for initial as well as loose semantics. In this paper we redefine vertical and different kinds of horizontal compositions using the new concept of semi-pushout defined for a mixture of signature and specification morphisms. The main results concerning correctness of horizontal...
Countable nondeterminism and logics of programs: fair-wellfoundedness of while-programs with nondeterministic assignments in the logic ALNA