Context-Aware Temporal Logic for Probabilistic Systems
Logic in Computer Science
2020-07-14 v1 Formal Languages and Automata Theory
Abstract
In this paper, we introduce the context-aware probabilistic temporal logic (CAPTL) that provides an intuitive way to formalize system requirements by a set of PCTL objectives with a context-based priority structure. We formally present the syntax and semantics of CAPTL and propose a synthesis algorithm for CAPTL requirements. We also implement the algorithm based on the PRISM-games model checker. Finally, we demonstrate the usage of CAPTL on two case studies: a robotic task planning problem, and synthesizing error-resilient scheduler for micro-electrode-dot-array digital microfluidic biochips.
Cite
@article{arxiv.2007.05793,
title = {Context-Aware Temporal Logic for Probabilistic Systems},
author = {Mahmoud Elfar and Yu Wang and Miroslav Pajic},
journal= {arXiv preprint arXiv:2007.05793},
year = {2020}
}