Context-Aware Temporal Logic for Probabilistic Systems

TL;DR

This paper introduces CAPTL, a new logic for formalizing probabilistic system requirements with context-based priorities, along with a synthesis algorithm and practical case studies demonstrating its application.

Contribution

The paper presents CAPTL, a novel probabilistic temporal logic with context-aware priorities, and provides a synthesis algorithm implemented in PRISM-games for real-world scenarios.

Findings

Successful formalization of system requirements using CAPTL

Effective synthesis algorithm demonstrated on case studies

Enhanced modeling of priorities in probabilistic systems

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.