A note on negative tagging for least fixed-point formulae
A Note on Negative Tagging for Least Fixed-Point Formulae
Proof systems with sequents of the form U ⊢ Φ for proving validity of a propositional modal μ-calculus formula Φ over a set U of states in a given model usually handle fixed-point formulae through unfolding, thus allowing such formulae to reappear in a proof. Tagging is a technique originated by Winskel for annotating fixed-point formulae with information about the proof states at which these are unfolded. This information is used later in the proof to avoid unnecessary unfolding, without...
À propos de la sémantique de l'appel par valeur selon A. Arnold
A selection property of the boolean -calculus and some of its applications
A system for deduction-based formal verification of workflow-oriented software models
The work concerns formal verification of workflow-oriented software models using the deductive approach. The formal correctness of a model's behaviour is considered. Manually building logical specifications, which are regarded as a set of temporal logic formulas, seems to be a significant obstacle for an inexperienced user when applying the deductive approach. A system, along with its architecture, for deduction-based verification of workflow-oriented models is proposed. The process inference is...
A theory of complexity of monadic recursion schemes
A theory of software reusability
About the decision of reachability for register machines
We study the decidability of the following problem: given affine functions over and two vectors , is reachable from by successive iterations of (in this given order)? We show that this question is decidable for and undecidable for some fixed .
About the decision of reachability for register machines
We study the decidability of the following problem: given p affine functions ƒ1,...,ƒp over and two vectors , is v2 reachable from v1 by successive iterations of ƒ1,...,ƒp (in this given order)? We show that this question is decidable for p = 1, 2 and undecidable for some fixed p.
Adjunction models for call-by-push-value with stacks.
Agent-oriented abstraction.
We define an agent-oriented abstraction formalism devoted to generalized theories of abstraction that have been proposed in Artificial Intelligence. The model we propose extends the abstraction capabilities of the existing Agent-Oriented Programming paradigm. This short note reviews first the existing attempts to define abstraction in AI and in agent systems. Then, our model is introduced in terms of six definitions covering the concepts of agents, annotated knowledge, utility and society of agents....
An algebraic treatment of flow diagrams and its application to generalized recursion theory
An specification language for fuzzy systems.
This work presents the main features of XFL3, a language for fuzzy system specification, which has been defined as the common description languaje for the tools forming the Xfuzzy 3.0 development environment. Its main advantages are its capability to admit user-defined membership functions, parametric operators, and linguistic hedges. A brief summary of the tools included in Xfuzzy 3.0 and an example illustrating the use of XFL3 are also included.
Approximate Model Checking of Real-Time Systems for Linear Duration Invariants
Real-time systems are usually modelled with timed automata and real-time requirements relating to the state durations of the system are often specifiable using Linear Duration Invariants, which is a decidable subclass of Duration Calculus formulas. Various algorithms have been developed to check timed automata or real-time automata for linear duration invariants, but each needs complicated preprocessing and exponential calculation. To the best of our knowledge, these algorithms have not been implemented....
Arbres infinis et systèmes d'équations
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....