Hyperproperties allow one to specify properties of systems that inherently involve not single executions of the system, but several of them at once: observational determinism and non-inference are two examples of such properties used to study the security of systems. Logics like HyperLTL have been studied in the past to model check hyperproperties of systems. However, most of the time, requiring strict security properties is actually ineffective as systems do not meet such requirements. To overcome this issue, we introduce qualitative reasoning in HyperLTL, inspired by a similar work on LTL by Almagor, Boker and Kupferman where a formula has a value in the interval [0, 1], obtained by considering either a propositional quality (how much the specification is satisfied), or a temporal quality (when the specification is satisfied). We show decidability of the approximated model checking problem, as well as the model checking of large fragments.

The Kleene theorem establishes a fundamental link between automata and expressions over the free monoid. Numerous generalisations of this result exist in the literature; on one hand, lifting this result to a weighted setting has been widely studied. On the other hand, beyond the free monoid, different monoids can be considered: for instance, two-way automata, and even tree-walking automata, can be described by expressions using the free inverse monoid. In the present work, we aim at combining both research directions and consider weighted extensions of automata and expressions over a class of monoids that we call pre-rational, generalising both the free inverse monoid and graded monoids. The presence of idempotent elements in these pre-rational monoids leads in the weighted setting to consider infinite sums. To handle such sums, we will have to restrict ourselves to rationally additive semirings. Our main result is thus a generalisation of the Kleene theorem for pre-rational monoids and rationally additive semirings. As a corollary, we obtain a class of expressions equivalent to weighted two-way automata, as well as one for tree-walking automata.

Abstract In this paper, we investigate the complexity of the emptiness problem for Parikh automata equipped with a pushdown stack. Pushdown Parikh automata extend pushdown automata with counters which can only be incremented and an acceptance condition given as a semi-linear set, which we represent as an existential Presburger formula over the final values of the counters. We show that the non-emptiness problem both in the deterministic and non-deterministic cases is . If the input head can move in a two-way fashion, emptiness gets undecidable, even if the pushdown stack is visibly and the automaton deterministic. We define a restriction, called the single-use restriction, to recover decidability in the presence of two-wayness, when the stack is visibly. This syntactic restriction enforces that any transition which increments at least one dimension is triggered only a bounded number of times per input position. Our main contribution is to show that non-emptiness of two-way visibly Parikh automata which are single-use is NExpTime-c . We finally give applications to decision problems for expressive transducer models from nested words to words, including the equivalence problem.

Cost register automata (CRA) are machines reading an input word while computing values using write-only registers: values from registers are combined using the two operations, as well as the constants, of a semiring. Particularly interesting is the subclass of copyless CRAs where the content of a register cannot be used twice for updating the registers. Originally deterministic, non-deterministic variant of CRA may also be defined: the semantics is then obtained by combining the values of all accepting runs with the additive operation of the semiring (as for weighted automata). We show that finitely-ambiguous copyless non-deterministic CRAs (i.e. the ones that admit a bounded number of accepting runs on every input word) can be effectively transformed into an equivalent copyless (deterministic) CRA, without requiring any specific property on the semiring. As a corollary, this also shows that regular look-ahead can effectively be removed from copyless CRAs.

Automata-logic connections are pillars of the theory of regular languages. Such connections are harder to obtain for transducers, but important results have been obtained recently for word-to-word transformations, showing that the three following models are equivalent: deterministic two-way transducers, monadic second-order (MSO) transducers, and deterministic one-way automata equipped with a finite number of registers. Nested words are words with a nesting structure, allowing to model unranked trees as their depth-first-search linearisations. In this paper, we consider transformations from nested words to words, allowing in particular to produce unranked trees if output words have a nesting structure. The model of visibly pushdown transducers allows to describe such transformations, and we propose a simple deterministic extension of this model with two-way moves that has the following properties: i) it is a simple computational model, that naturally has a good evaluation complexity; ii) it is expressive: it subsumes nested word-to-word MSO transducers, and the exact expressiveness of MSO transducers is recovered using a simple syntactic restriction; iii) it has good algorithmic/closure properties: the model is closed under composition with a unambiguous one-way letter-to-letter transducer which gives closure under regular look-around, and has a decidable equivalence problem.

Weighted automata (WA) extend finite-state automata by associating with transitions weights from a semiring S, defining functions from words to S. Recently, cost register automata (CRA) have been introduced as an alternative model to describe any function realised by a WA by means of a deterministic machine. Unambiguous WA over a monoid (M, ⊗) can equivalently be described by cost register automata whose registers take their values in M, and are updated by operations of the form x: = y ⊗ c, with c ∈ M. This class is denoted by CRA⊗c(M).

Administration of access control policies is a difficult task, especially in large organizations. We consider the problem of detecting whether administrative actions can yield in policies where some security goals are compromised. In particular, we are interested in problems generated by modifications --- such as adding/deleting elements to/from the set of possible users or permissions --- of policies specified as term-rewrite systems. We propose to use rewriting techniques to compare the behaviors of the modified version and the original version of the policy. More precisely, we use narrowing to compute counter-examples to the equivalence of rewrite-based policies. We prove that our technique provides a sound and complete way to recursively enumerate the set of counter-examples, even when this set is not finite, or when a mistake of the administrator makes one or both systems non-terminating.

Variables are the distinguishing new feature of XPath 2.0 which permits to select n-tuples of nodes in trees. It is known that the Core of XPath 2.0 captures n-ary first-order (FO) queries modulo linear time transformations. In this paper, we distinguish a fragment of Core XPath 2.0 that remains FO-complete with respect ton-ary queries while enjoying polynomial-time query answering.

In this paper we investigate the quantifier-free fragment of the TQL logic proposed by Cardelli and Ghelli. The TQL logic, inspired from the ambient logic, is the core of a query language for semistructured data represented as unranked and unordered trees. The fragment we consider here, named STL, contains as main features spatial composition and location as well as a fixed point construct. We prove that satisfiability for STL is undecidable. We show also that STL is strictly more expressive than the Presburger monadic second-order logic (PMSO) of Seidl, Schwentick and Muscholl when interpreted over unranked and unordered edge-labelled trees. We define a class of tree automata whose transitions are conditioned by arithmetical constraints; we show then how to compute from a closed STL formula a tree automaton accepting precisely the models of the formula. Finally, still using our tree automata framework, we exhibit some syntactic restrictions over STL formulae that allow us to capture precisely the logics MSO and PMSO.

Set-based analysis of logic programs provides an accurate method for descriptive type-checking of logic programs. The key idea of this method is to upper approximate the least model of the program by a regular set of trees. In 1991, Frühwirth, Shapiro, Vardi and Yardeni raised the question whether it can be more efficient to use the domain of sets of paths instead, i.e., to approximate the least model by a regular set of words. We answer the question negatively by showing that type-checking for path-based analysis is as hard as the set-based one, that is DEXPTIME-complete. This result has consequences also in the areas of set constraints, automata theory and model checking.

The complexity of set constraints has been extensively studied over the last years and was often found quite high. At the lower end of expressiveness, there are atomic set constraints which are conjunctions of inclusions t/sub 1//spl sube/t/sub 2/ between first-order terms without set operators. It is well-known that satisfiability of atomic set constraints can be tested in cubic time. Also, entailment of atomic set constraints has been claimed decidable in polynomial time. We refute this claim. We show that entailment between atomic set constraints can express validity of quantified boolean formulas and is this PSPACE hard. For infinite signatures, we also present a PSPACE-algorithm for solving atomic set constraints with negation. This proves that entailment of atomic set constraints is PSPACE-complete for infinite signatures. In case of finite signatures, this problem is even DEXPTIME-hard.