### A note on negative tagging for least fixed-point formulae

Skip to main content (access key 's'),
Skip to navigation (access key 'n'),
Accessibility information (access key '0')

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...

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...

We study the decidability of the following problem: given $p$ affine functions ${f}_{1},...,{f}_{p}$ over ${\mathbb{N}}^{k}$ and two vectors ${v}_{1},{v}_{2}\in {\mathbb{N}}^{k}$, is ${v}_{2}$ reachable from ${v}_{1}$ by successive iterations of ${f}_{1},...,{f}_{p}$ (in this given order)? We show that this question is decidable for $p=1,2$ and undecidable for some fixed $p$.

We study the decidability of the following problem: given p affine functions ƒ1,...,ƒp over ${\mathbb{N}}^{k}$ and two vectors ${v}_{1},{v}_{2}\in {\mathbb{N}}^{k}$, 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.

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....

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.

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....

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...

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....