The Hierarchy of Hyperlogics
Autor: | Bernd Finkbeiner, Norine Coenen, Jana Hofmann, Christopher Hahn |
---|---|
Rok vydání: | 2019 |
Předmět: |
Discrete mathematics
FOS: Computer and information sciences Computer Science - Logic in Computer Science Hierarchy (mathematics) F.4 Order (ring theory) 020207 software engineering 02 engineering and technology Predicate (mathematical logic) 16. Peace & justice Undecidable problem Decidability Logic in Computer Science (cs.LO) TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Path (graph theory) 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Boolean satisfiability problem Mathematics TRACE (psycholinguistics) |
Zdroj: | 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) LICS |
DOI: | 10.1109/lics.2019.8785713 |
Popis: | Hyperproperties, which generalize trace properties by relating multiple traces, are widely studied in information-flow security. Recently, a number of logics for hyperproperties have been proposed, and there is a need to understand their decidability and relative expressiveness. The new logics have been obtained from standard logics with two principal extensions: temporal logics, like LTL and CTL$^*$, have been generalized to hyperproperties by adding variables for traces or paths. First-order and second-order logics, like monadic first-order logic of order and MSO, have been extended with the equal-level predicate. We study the impact of the two extensions across the spectrum of linear-time and branching-time logics, in particular for logics with quantification over propositions. The resulting hierarchy of hyperlogics differs significantly from the classical hierarchy, suggesting that the equal-level predicate adds more expressiveness than trace and path variables. Within the hierarchy of hyperlogics, we identify new boundaries on the decidability of the satisfiability problem. Specifically, we show that while HyperQPTL and HyperCTL$^*$ are both undecidable in general, formulas within their $\exists^*\forall^*$ fragments are decidable. Comment: Originally published at LICS 2019 |
Databáze: | OpenAIRE |
Externí odkaz: |