Concurrent Dynamic Algebra
- Submitting institution
-
The University of Sheffield
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 2478
- Type
- D - Journal article
- DOI
-
10.1145/2785967
- Title of journal
- ACM Transactions on Computational Logic
- Article number
- 30
- First page
- 1
- Volume
- 16
- Issue
- 4
- ISSN
- 1529-3785
- Open access status
- Out of scope for open access requirements
- Month of publication
- August
- Year of publication
- 2015
- 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
-
1
- Research group(s)
-
I - Verification
- Citation count
- 4
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- First algebraic study of concurrent dynamic logics, as proposed by Peled, Goldblatt and Nerode, and sheds new light on underlying multirelational semantics. Such formalisms are important for analysing games, programs with alternating non-determinism and hybrid systems. Follow-up articles published in journals (ACM TOCL: doi.org/10.1145/2964907, JLAMP: doi.org/10.1016/j.jlamp.2017.04.002, MSCS: doi.org/10.1017/S096012951700007X). Approach has been formalised with the Isabelle/HOL proof assistant. Groups in Germany, Japan, New Zealand and Portugal have continued this line of work (e.g. doi.org/10.1007/978-3-030-38808-9_14, https://www.sciencedirect.com/science/article/pii/S2352220817300263). Work was funded by the Royal Society. Led to two JSPS grants (KAKENHI 25330016 and 16K21557), which supported the JLAMP paper and further joint work.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -