Related papers: Problems parameterized by treewidth tractable in s…
Temporal logic is a very powerful formalism deeply investigated and used in formal system design and verification. Its application usually reduces to solving specific decision problems such as model checking and satisfiability. In these…
Ability to count number of occurrences of events within a specified time interval is very useful in specification of resource bounded real time computation. In this paper, we study an extension of Metric Temporal Logic ($\mathsf{MTL}$) with…
In this paper, we introduce a novel algorithm to solve projected model counting (PMC). PMC asks to count solutions of a Boolean formula with respect to a given set of projected variables, where multiple solutions that are identical when…
We introduce a logical foundation to reason on tree structures with constraints on the number of node occurrences. Related formalisms are limited to express occurrence constraints on particular tree regions, as for instance the children of…
In this paper, we introduce a novel algorithm to solve projected model counting (PMC). PMC asks to count solutions of a Boolean formula with respect to a given set of projection variables, where multiple solutions that are identical when…
We consider the satisfiability problem for the two-variable fragment of the first-order logic extended with modulo counting quantifiers and interpreted over finite words or trees. We prove a small-model property of this logic, which gives a…
Probabilistic argumentation allows reasoning about argumentation problems in a way that is well-founded by probability theory. However, in practice, this approach can be severely limited by the fact that probabilities are defined by adding…
Regular tree grammars and regular path expressions constitute core constructs widely used in programming languages and type systems. Nevertheless, there has been little research so far on frameworks for reasoning about path expressions…
Many tractable algorithms for solving the Constraint Satisfaction Problem (CSP) have been developed using the notion of the treewidth of some graph derived from the input CSP instance. In particular, the incidence graph of the CSP instance…
In this paper, we consider counting and projected model counting of extensions in abstract argumentation for various semantics. When asking for projected counts we are interested in counting the number of extensions of a given argumentation…
A breakthrough result of Cygan et al. (FOCS 2011) showed that connectivity problems parameterized by treewidth can be solved much faster than the previously best known time $\mathcal{O}^*(2^{\mathcal{O}(tw \log(tw))})$. Using their inspired…
Algorithmic meta-theorems state that problems definable in a fixed logic can be solved efficiently on structures with certain properties. An example is Courcelle's Theorem, which states that all problems expressible in monadic second-order…
Characterisations theorems serve as important tools in model theory and can be used to assess and compare the expressive power of temporal languages used for the specification and verification of properties in formal methods. While complete…
Adding propositional quantification to the modal logics K, T or S4 is known to lead to undecidability but CTL with propositional quantification under the tree semantics (tQCTL) admits a non-elementary Tower-complete satisfiability problem.…
Possibilistic computation tree Logic (PoCTL) is one kind of branching temporal logic combined with uncertain information in possibility theory, which was introduced in order to cope with the systematic verification on systems with uncertain…
We introduce a generic extension of the popular branching-time logic CTL which refines the temporal until and release operators with formal languages. For instance, a language may determine the moments along a path that an until property…
The problem of deciding whether CSP instances admit solutions has been deeply studied in the literature, and several structural tractability results have been derived so far. However, constraint satisfaction comes in practice as a…
Regular tree grammars and regular path expressions constitute core constructs widely used in programming languages and type systems. Nevertheless, there has been little research so far on reasoning frameworks for path expressions where node…
This paper presents a range of quantitative extensions for the temporal logic CTL. We enhance temporal modalities with the ability to constrain the number of states satisfying certain sub-formulas along paths. By selecting the combinations…
This thesis describes the theoretical and practical foundations of a system for the static analysis of XML processing languages. The system relies on a fixpoint temporal logic with converse, derived from the mu-calculus, where models are…