Optimal repair for omega-regular properties

DOI10.1007/978-3-031-19992-9_23MaRDI QIDQ6160923zbMATH OpenOpenAlexFDO

Authors Vrunda Dave, Shankara Narayanan Krishna, Ashutosh Trivedi

Publication date 2 June 2023

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2207.13416

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: This paper presents an optimization based framework to automate system repair against omega-regular properties. In the proposed formalization of optimal repair, the systems are represented as Kripke structures, the properties as $omega$-regular languages, and the repair space as repair machines -- weighted omega-regular transducers equipped with B"uchi conditions -- that rewrite strings and associate a cost sequence to these rewritings. To translate the resulting cost-sequences to easily interpretable payoffs, we consider several aggregator functions to map cost sequences to numbers -- including limit superior, supremum, discounted-sum, and average-sum -- to define quantitative cost semantics. The problem of optimal repair, then, is to determine whether traces from a given system can be rewritten to satisfy an $omega$-regular property when the allowed cost is bounded by a given threshold. We also consider the dual challenge of impair verification that assumes that the rewritings are resolved adversarially under some given cost restriction, and asks to decide if all traces of the system satisfy the specification irrespective of the rewritings. With a negative result to the impair verification problem, we study the problem of designing a minimal mask of the Kripke structure such that the resulting traces satisfy the specifications despite the threshold-bounded impairment. We dub this problem as the mask synthesis problem. This paper presents automata-theoretic solutions to repair synthesis, impair verification, and mask synthesis problem for limit superior, supremum, discounted-sum, and average-sum cost semantics.

Recommendations

• Optimal fixed-premise repairs of \(\mathcal{E}\mathcal{L}\) TBoxes
• Some properties and computational results for a general repair process
• Computing optimal repairs of quantified ABoxes w.r.t. static \(\mathcal{EL}\) TBoxes
• OPTIMAL REPAIR OF A SERIES SYSTEM WITH FIXED REPAIR TIMES
• An optimal proportion of perfect repair
• scientific article; zbMATH DE number 1334316

Cites work

• scientific article; zbMATH DE number 700091 (Why is no real title available?)
• scientific article; zbMATH DE number 7559473 (Why is no real title available?)
• A Survey of Stochastic Games with Limsup and Liminf Objectives
• Comparator automata in quantitative verification
• Computer Aided Verification
• Coping with selfish on-going behaviors
• Expressiveness and closure properties for quantitative languages
• From model checking to model measuring
• Program repair without regret
• Quantitative Languages
• Quantitative fair simulation games
• The complexity of mean payoff games on graphs

This page was built for publication: Optimal repair for omega-regular properties

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6160923)