arXiv subjects

Aggeliki Chalki

Publications and source records attributed to Aggeliki Chalki.

6 recordsLinked to original sources

arXiv2025

The Complexity of Deciding Characteristic Formulae Modulo Nested Simulation (extended abstract)

This paper studies the complexity of determining whether a formula in the modal logics characterizing the nested-simulation semantics is characteristic for some process, which is equivalent to determining whether the formula is satisfiable and prime. The main results are that the problem of determining whether a formula is prime in the modal logic characterizing the 2-nested-simulation preorder is coNP-complete and is PSPACE-complete in the case of the n-nested-simulation preorder, when n>=3. This establishes that deciding characteristic formulae for the n-nested simulation semantics is PSPACE-complete, when n>=3. In the case of the 2-nested simulation semantics, that problem lies in the complexity class DP, which consists of languages that can be expressed as the intersection of one language in NP and of one in coNP.

cs.LO↗

arXiv2025

Deciding characteristic formulae: A journey in the branching-time spectrum

Characteristic formulae give a complete logical description of the behaviour of processes modulo some chosen notion of behavioural semantics. They allow one to reduce equivalence or preorder checking to model checking, and are exactly the formulae in the modal logics characterizing classic behavioural equivalences and preorders for which model checking can be reduced to equivalence or preorder checking. This paper studies the complexity of determining whether a formula is characteristic for some process in each of the logics providing modal characterizations of the simulation-based semantics in van Glabbeek's branching-time spectrum. Since characteristic formulae in each of those logics are exactly the satisfiable and prime ones, this article presents complexity results for the satisfiability and primality problems, and investigates the boundary between modal logics for which those problems can be solved in polynomial time and those for which they become (co)NP- or PSPACE-complete.

cs.LO↗

arXiv2024

The complexity of deciding characteristic formulae in van Glabbeek's branching-time spectrum

Characteristic formulae give a complete logical description of the behaviour of processes modulo some chosen notion of behavioural semantics. They allow one to reduce equivalence or preorder checking to model checking, and are exactly the formulae in the modal logics characterizing classic behavioural equivalences and preorders for which model checking can be reduced to equivalence or preorder checking. This paper studies the complexity of determining whether a formula is characteristic for some finite, loop-free process in each of the logics providing modal characterizations of the simulation-based semantics in van Glabbeek's branching-time spectrum. Since characteristic formulae in each of those logics are exactly the consistent and prime ones, it presents complexity results for the satisfiability and primality problems, and investigates the boundary between modal logics for which those problems can be solved in polynomial time and those for which they become computationally hard. Amongst other contributions, this article also studies the complexity of constructing characteristic formulae in the modal logics characterizing simulation-based semantics, both when such formulae are presented in explicit form and via systems of equations.

cs.LO↗

arXiv2024

On the power of counting the total number of computation paths of NPTMs

In this paper, we define and study variants of several complexity classes of decision problems that are defined via some criteria on the number of accepting paths of an NPTM. In these variants, we modify the acceptance criteria so that they concern the total number of computation paths instead of the number of accepting ones. This direction reflects the relationship between the counting classes #P and TotP, which are the classes of functions that count the number of accepting paths and the total number of paths of NPTMs, respectively. The former is the well-studied class of counting versions of NP problems introduced by Valiant (1979). The latter contains all self-reducible counting problems in #P whose decision version is in P, among them prominent #P-complete problems such as Non-negative Permanent, #PerfMatch, and #DNF-Sat, thus playing a significant role in the study of approximable counting problems. We show that almost all classes introduced in this work coincide with their `#accepting paths'-definable counterparts, thus providing an alternative model of computation for them. Moreover, for each of these classes, we present a novel family of complete problems, which are defined via TotP-complete problems. This way, we show that all the aforementioned classes have complete problems that are defined via counting problems whose existence version is in P, in contrast to the standard way of obtaining completeness results via counting versions of NP-complete problems. To the best of our knowledge, prior to this work, such results were known only for parity-P and C=P.

cs.CC↗

arXiv2023

Counting Computations with Formulae: Logical Characterisations of Counting Complexity Classes

We present quantitative logics with two-step semantics based on the framework of quantitative logics introduced by Arenas et al. (2020) and the two-step semantics defined in the context of weighted logics by Gastin & Monmege (2018). We show that some of the fragments of our logics augmented with a least fixed point operator capture interesting classes of counting problems. Specifically, we answer an open question in the area of descriptive complexity of counting problems by providing logical characterizations of two subclasses of #P, namely SpanL and TotP, that play a significant role in the study of approximable counting problems. Moreover, we define logics that capture FPSPACE and SpanPSPACE, which are counting versions of PSPACE.

cs.LO↗

arXiv2020

Characterizations and approximability of hard counting classes below #P

An important objective of research in counting complexity is to understand which counting problems are approximable. In this quest, the complexity class TotP, a hard subclass of #P, is of key importance, as it contains self-reducible counting problems with easy decision version, thus eligible to be approximable. Indeed, most problems known so far to admit an fpras fall into this class. An open question raised recently by the community of descriptive complexity is to find a logical characterization of TotP and of robust subclasses of TotP. In this work we define two subclasses of TotP, in terms of descriptive complexity, both of which are robust in the sense that they have natural complete problems, which are defined in terms of satisfiability of Boolean formulae. We then explore the relationship between the class of approximable counting problems and TotP. We prove that TotP $\nsubseteq$ FPRAS if and only if NP $\neq$ RP and FPRAS $\nsubseteq$ TotP unless RP = P. To this end we introduce two ancillary classes that can both be seen as counting versions of RP. We further show that FPRAS lies between one of these classes and a counting version of BPP. Finally, we provide a complete picture of inclusions among all the classes defined or discussed in this paper with respect to different conjectures about the NP vs. RP vs. P questions.

cs.CC↗