Branching-time logic ECTL# and its tree-style one-pass tableau: Extending fairness expressibility of ECTL+
- Submitting institution
-
The University of Westminster
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- qy9vw
- Type
- D - Journal article
- DOI
-
10.1016/j.tcs.2020.02.015
- Title of journal
- Theoretical Computer Science
- Article number
- -
- First page
- 428
- Volume
- 813
- Issue
- -
- ISSN
- 0304-3975
- Open access status
- Compliant
- Month of publication
- February
- Year of publication
- 2020
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
2
- Research group(s)
-
-
- Citation count
- 0
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Fairness required for Safety Critical Software, should realise infinitely often a dedicated class of periodic events; when periodicity involves the eventuality “until”, a new, challenging case of fairness arises. This article is significant because it (1) solved the challenge introducing a new expressive computation tree logic (2) defined a roadmap, a novel reasoning technique for generating both verifications and proofs as certificates. These have prompted more relevant results (https://www.ehu.eus/en/web/lorea), collaborative application for funding supported by industrial interest. Evidence can be obtained from J.L. Martín González, VC for Research, University of Basque Country (vrinvestigacion@ehu.eus); Jorge Parra, Ikerlan Technology Research Centre (JParra@ikerlan.es).
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
