Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\)
type: Item
instance of: scholarly article
title: Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\)
zbMATH Open document ID: 1433.03049
author: Alexander Bolotov
author: M. Hermo
author: P. Lucio
published in: Theoretical Computer Science
publication date: 2020-04-21T00:00:00Z
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 7191326
zbMATH Keywords: temporal logic
zbMATH Keywords: fairness
zbMATH Keywords: tableau
zbMATH Keywords: branching-time
zbMATH Keywords: one-pass tableau
describes a project that uses: TTM
describes a project that uses: Rabinizer
MaRDI profile type: Publication
full work available at URL: j.tcs.2020.02.015
OpenAlex ID: W3006352198
cites work: Decision procedures and expressiveness in the temporal logic of branching time
cites work: “Sometimes” and “not never” revisited
cites work: Automatic verification of finite-state concurrent systems using temporal logic specifications
cites work: Q3761688
cites work: Q4722045
cites work: Model-based testing of reactive systems. Advanced lectures.
cites work: Rabinizer 2: Small Deterministic Automata for LTL ∖ GU
cites work: Q4385542
cites work: Cut-free sequent systems for temporal logic
cites work: Dual systems of tableaux and sequents for PLTL
cites work: One-Pass Tableaux for Computation Tree Logic
cites work: A Decision Procedure for CTL* Based on Tableaux and Automata
cites work: Q4484475
cites work: Rewrite rules for \(\mathrm{CTL}^\ast\)
cites work: FM 2009: Formal methods. Second world congress, Eindhoven, The Netherlands, November 2--6, 2009. Proceedings
cites work: A tableau-based decision procedure for CTL\(^*\)
cites work: Tableau methods for modal and temporal logics
cites work: Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach
cites work: Q3219755
cites work: An automata-theoretic approach to branching-time model checking
DOI: 10.1016/J.TCS.2020.02.015
description: scientific article; zbMATH DE number 7191326