Markus Latte

dblp:94/8262 · DBLP profile ↗
← Back
4ranked-venue papers
3as first author
1since 2021 · last 2021
0000-0002-6583-1273ORCID · verified

Domains — the database's venue-derived domains; a paper can count in several

Theory of computation · 4 · 3 first-author · 1 since 2021
YearPublicationVenuePosition
2021 Branching-time logics and fairness, revisited
abstract
Abstract Emerson and Halpern (1986,Journal of the Association for Computing Machinery33, 151–178) prove that the Computation Tree Logic (CTL) cannot express the existence of a path on which a proposition holds infinitely often (fairness for short). The scope is widened fromCTLto a general branching-time logic. A path quantifier is followed by a language with temporal descriptions. In this extended setting, the said inexpressiveness is strengthened in two aspects. First, universal path quantifiers are unrestricted. In this way, they are relieved of any temporal quantifiers such as of those in $\mathtt{AU}$ and $\mathtt{AR}$ fromCTL. Second, existential path quantifiers are allowed with any countable language. Instances are the temporal quantifiers in $\mathtt{EU}$ and $\mathtt{ER}$ fromCTL. By contrast, the fairness statement is an existential path quantifier with an uncountable language. Both aspects indicate that this inexpressiveness is optimal with respect to the polarity of path quantifiers and to the cardinality of their languages.
Markus Latte
Math. Struct. Comput. Sci.1
2015 Definability by Weakly Deterministic Regular Expressions with Counters is Decidable
Markus Latte, Matthias Niewerth
MFCS (1)1
2014 Branching-time logics with path relativisation
Markus Latte, Martin Lange 0001
J. Comput. Syst. Sci.1
2010 A CTL-Based Logic for Program Abstractions
Martin Lange 0001, Markus Latte
WoLLIC2