Displaying similar documents to “On characteristic formulae for Event-Recording Automata”

Characteristic Formulae for Timed Automata

Luca Aceto, Anna Ingólfsdóttir, Mikkel Lykke Pedersen, Jan Poulsen (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

This paper offers characteristic formula constructions in the real-time logic 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...

On Core XPath with Inflationary Fixed Points

Loredana Afanasiev, Balder Ten Cate (2013)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

Similarity:

We prove the undecidability of Core XPath 1.0 (CXP) [G. Gottlob and C. Koch, in IEEE CS Press (2002) 189–202.] extended with an operator. More specifically, we prove that the satisfiability problem of this language is undecidable. In fact, the fragment of CXP+IFP containing only the and axes is already undecidable.

Inf-datalog, Modal Logic and Complexities

Eugénie Foustoucos, Irène Guessarian (2007)

RAIRO - Theoretical Informatics and Applications

Similarity:

Inf-Datalog extends the usual least fixpoint semantics of Datalog with greatest fixpoint semantics: we defined inf-Datalog and characterized the expressive power of various fragments of inf-Datalog in [CITE]. In the present paper, we study the complexity of query evaluation on finite models for (various fragments of) inf-Datalog. We deduce a unified and elementary proof that global model-checking ( computing all nodes satisfying a formula in a given structure) has 1. quadratic...

Universality of Reversible Hexagonal Cellular Automata

Kenichi Morita, Maurice Margenstern, Katsunobu Imai (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

We define a kind of cellular automaton called a hexagonal partitioned cellular automaton (HPCA), and study logical universality of a reversible HPCA. We give a specific 64-state reversible HPCA , and show that a Fredkin gate can be embedded in this cellular space. Since a Fredkin gate is known to be a universal logic element, logical universality of is concluded. Although the number of states of is greater than those of the previous...

Topologies, Continuity and Bisimulations

J. M. Davoren (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

The notion of a is of basic importance in many areas of computation theory and logic. Of late, it has come to take a particular significance in work on the formal analysis and verification of , where system properties are expressible by formulas of the modal -calculus or weaker temporal logics. Our purpose here is to give an analysis of the concept of bisimulation, starting with the observation that the zig-zag conditions are suggestive of some form of continuity. We give a topological...

Comparing the succinctness of monadic query languages over finite trees

Martin Grohe, Nicole Schweikardt (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

We study the of monadic second-order logic and a variety of monadic fixed point logics on trees. All these languages are known to have the same expressive power on trees, but some can express the same queries much more succinctly than others. For example, we show that, under some complexity theoretic assumption, monadic second-order logic is non-elementarily more succinct than monadic least fixed point logic, which in turn is non-elementarily more succinct than monadic datalog.
Succinctness...

New applications of the wreath product of forest algebras

Howard Straubing (2013)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

Similarity:

We give several new applications of the wreath product of forest algebras to the study of logics on trees. These include new simplified proofs of necessary conditions for definability in and first-order logic with the ancestor relation; a sequence of identities satisfied by all forest languages definable in ; and new examples of languages outside along with an application to the question of what properties are definable in both and

Domain mu-calculus

Guo-Qiang Zhang (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

The basic framework of domain -calculus was formulated in [39] more than ten years ago. This paper provides an improved formulation of a fragment of the -calculus without function space or powerdomain constructions, and studies some open problems related to this -calculus such as decidability and expressive power. A class of language equations is introduced for encoding -formulas in order to derive results related to decidability and expressive power of non-trivial fragments of the...