Safraless Synthesis for Epistemic Temporal Specifications

TL;DR

This paper introduces a new, more efficient 'Safraless' synthesis method for single-agent systems with epistemic temporal logic specifications, avoiding complex automata constructions and enabling practical applications.

Contribution

It presents a novel Safraless synthesis approach for KLTL specifications, transforming the problem into automata emptiness checking and safety game solving, improving efficiency.

Findings

Implemented the method and demonstrated its effectiveness on case studies.

Achieved more practical synthesis procedures for epistemic temporal logic.

Reduced complexity compared to traditional automata-based approaches.

Abstract

In this paper we address the synthesis problem for specifications given in linear temporal single-agent epistemic logic, KLTL (or $KL_1$), over single-agent systems having imperfect information of the environment state. Van der Meyden and Vardi have shown that this problem is 2Exptime complete. However, their procedure relies on complex automata constructions that are notoriously resistant to efficient implementations as they use Safra-like determinization. We propose a "Safraless" synthesis procedure for a large fragment of KLTL. The construction transforms first the synthesis problem into the problem of checking emptiness for universal co-B\"{u}chi tree automata using an information-set construction. Then we build a safety game that can be solved using an antichain-based symbolic technique exploiting the structure of the underlying automata. The technique is implemented and applied to a couple of case studies.