arXiv subjects

Vishnu Murali

Publications and source records attributed to Vishnu Murali.

10 recordsLinked to original sources

arXiv2026

HyperCertificates: Verification of Discrete-time Dynamical Systems against HyperLTL Specifications

We introduce a functional inductive framework to verify discrete-time dynamical systems against hyperproperties specified as Hyperlinear temporal logic formulae via a notion of HyperCertificates. Unlike linear temporal logic (LTL) formulae which are concerned with individual traces of a system, hyperproperties are properties that are concerned with how the traces of a system relate to one another. HyperLTL is an extension of LTL for hyperproperties, and is useful to describe specifications such as opacity, privacy as well as notions of robustness. Our notion of HyperCertificates consists of a pair of functions, where the first models the lookahead, and the second relies on a combination of barrier and ranking functions. We use closure certificates, to act as a model for this lookahead and then rely on barrier and ranking function arguments modulo this lookahead to provide guarantees against HyperLTL formulae. We demonstrate how our approach is automatable via existing techniques such as sum-of-squares optimization (SOS) and satisfiability modulo theories (SMT) solvers. Finally, we demonstrate our approach on some case studies.

eess.SY↗

arXiv2026

Agentic Jackal: Live Execution and Semantic Value Grounding for Text-to-JQL

Translating natural language into Jira Query Language (JQL) requires resolving ambiguous field references, instance-specific categorical values, and complex Boolean predicates. Single-pass LLMs cannot discover which categorical values (e.g., component names or fix versions) actually exist in a given Jira instance, nor can they verify generated queries against a live data source, limiting accuracy on paraphrased or ambiguous requests. No open, execution-based benchmark exists for mapping natural language to JQL. We introduce Jackal, the first large-scale, execution-based text-to-JQL benchmark comprising 100,000 validated NL-JQL pairs on a live Jira instance with over 200,000 issues. To establish baselines on Jackal, we propose Agentic Jackal, a tool-augmented agent that equips LLMs with live query execution via the Jira MCP server and JiraAnchor, a semantic retrieval tool that resolves natural-language mentions of categorical values through embedding-based similarity search. Among 9 frontier LLMs evaluated, single-pass models average only 43.4% execution accuracy on short natural-language queries, highlighting that text-to-JQL remains an open challenge. The agentic approach improves 7 of 9 models, with a 9.0% relative gain on the most linguistically challenging variant; in a controlled ablation isolating JiraAnchor, categorical-value accuracy rises from 48.7% to 71.7%, with component-field accuracy jumping from 16.9% to 66.2%. Our analysis identifies inherent semantic ambiguities, such as issue-type disambiguation and text-field selection, as the dominant failure modes rather than value-resolution errors, pointing to concrete directions for future work. We publicly release the benchmark, all agent transcripts, and evaluation code to support reproducibility.

cs.CL↗

arXiv2026

Vector Certificates for $\omega$-regular Specifications

The recently introduced notions of ranking functions and closure certificates utilize well-foundedness arguments to facilitate the verification of dynamical systems against $\omega$-regular properties. A ranking function and a closure certificate are real-valued functions defined over states and state pairs of a dynamical system whose zero superlevel sets are inductive state invariant and inductive transition invariant, respectively. The search for such certificates can be automated by fixing a specific template class, such as a polynomial of a fixed degree, and then using optimization techniques such as sum-of-squares (SOS) programming to find it. Unfortunately, such certificates may not be found for a fixed template. In such a case, one must change the template; for example, increase the degree of the polynomial. In this paper, we consider a notion of multiple functions in the form of vector certificates. Taking inspiration from the literature on vector barrier certificates as generalizations of standard barrier certificates for safety verification, we propose vector co-B\"uchi ranking functions and vector closure certificates as nontrivial generalizations of ranking functions and closure certificates, respectively. Both notions consist of a set of functions that jointly overapproximate an inductive invariant by considering each function to be a linear combination of the others. The advantage of such certificates is that they allow us to prove properties even when a single function for a fixed template cannot be found using standard approaches. We present an SOS programming approach to search for these functions and demonstrate the effectiveness of our proposed method in verifying $\omega$-regular specifications in several case studies.

eess.SY↗

arXiv2026

Interpolation-Inspired Closure Certificates

Barrier certificates, a form of state invariants, provide an automated approach to the verification of the safety of dynamical systems. Similarly to barrier certificates, recent works explore the notion of closure certificates, a form of transition invariants, to verify dynamical systems against $\omega$-regular properties including safety. A closure certificate, defined over state pairs of a dynamical system, is a real-valued function whose zero superlevel set characterizes an inductive transition invariant of the system. The search for such a certificate can be effectively automated by assuming it to be within a specific template class, e.g. a polynomial of a fixed degree, and then using optimization techniques such as sum-of-squares (SOS) programming to find it. Unfortunately, one may not be able to find such a certificate for a fixed template. In such a case, one must change the template, e.g. increase the degree of the polynomial. In this paper, we consider a notion of multiple closure certificates dubbed interpolation-inspired closure certificates. An interpolation-inspired closure certificate consists of a set of functions which jointly over-approximate a transition invariant by first considering one-step transitions, then two, and so on until a transition invariant is obtained. The advantage of interpolation-inspired closure certificates is that they allow us to prove properties even when a single function for a fixed template cannot be found using standard approaches. We present SOS programming and a scenario program to find these sets of functions and demonstrate the effectiveness of our proposed method to verify persistence and general $\omega$-regular specifications in some case studies.

eess.SY↗

arXiv2025

Control Closure Certificates

This paper introduces the notion of control closure certificates to synthesize controllers for discrete-time control systems against $\omega$-regular specifications. Typical functional approaches to synthesize controllers against $\omega$-regular specifications rely on combining inductive invariants (for example, via barrier certificates) with proofs of well-foundedness (for example, via ranking functions). Transition invariants, provide an alternative where instead of standard well-foundedness arguments one may instead search for disjunctive well-foundedness arguments that together ensure a well-foundedness argument. Closure certificates, functional analogs of transition invariants, provide an effective, automated approach to verify discrete-time dynamical systems against linear temporal logic and $\omega$-regular specifications. We build on this notion to synthesize controllers to ensure the satisfaction of $\omega$-regular specifications. To do so, we first illustrate how one may construct control closure certificates to visit a region infinitely often (or only finitely often) via disjunctive well-founded arguments. We then combine these arguments to provide an argument for parity specifications. Thus, finding an appropriate control closure certificate over the product of the system and a parity automaton specifying a desired $\omega$-regular specification ensures that there exists a controller $\kappa$ to enforce the $\omega$-regular specification. We propose a sum-of-squares optimization approach to synthesize such certificates and demonstrate their efficacy in designing controllers over some case studies.

cs.LO↗

arXiv2025

$k$-Inductive and Interpolation-Inspired Barrier Certificates for Stochastic Dynamical Systems

In this paper, we introduce two new types of barrier certificates that are based on multiple functions rather than a single one. A conventional barrier certificate for a stochastic dynamical system is a nonnegative real-valued function whose expected value does not increase as the system evolves. This requirement guarantees that the barrier certificate forms a nonnegative supermartingale and can be used to derive a lower bound on the probability that the system remains safe. A key advantage of such certificates is that they can be automatically searched for using tools such as optimization programs instantiated with a fixed template. When this search is unsuccessful, the common practice is to modify the template and attempt the synthesis again. Drawing inspiration from logical interpolation, we first propose an alternative framework that uses a collection of functions to jointly serve as a barrier certificate. We refer to this construct as an interpolation-inspired barrier certificate. Nonetheless, we observe that these certificates still require one function in the collection to satisfy a supermartingale condition. Motivated by recent work in the literature, we next combine k-induction with interpolation-inspired certificates to relax this supermartingale constraint. We develop a general and more flexible notion of barrier certificates, which we call k-inductive interpolation-inspired barrier certificates. This formulation encompasses multiple ways of integrating interpolation-inspired barrier certificates with k-induction. We highlight two specific instantiations among these possible combinations. For polynomial systems, we employ sum-of-squares (SOS) programming to synthesize the corresponding set of functions. Finally, through our case studies, we show that the proposed methods enable the use of simpler templates and yield tighter lower bounds on the safety probability.

math.OC↗

arXiv2023

Co-Buchi Barrier Certificates for Discrete-time Dynamical Systems

Barrier certificates provide functional overapproximations for the reachable set of dynamical systems and provide inductive guarantees on the safe evolution of the system. In automata-theoretic verification, a key query is to determine whether the system visits a given predicate over the states finitely often, typically resulting from the complement of the traditional Buchi acceptance condition. This paper proposes a barrier certificate approach to answer such queries by developing a notion of co-Buchi barrier certificates (CBBCs) that generalize classic barrier certificates to ensure that the traces of a system visit a given predicate a fixed number of times. Our notion of CBBC is inspired from bounded synthesis paradigm to LTL realizability, where the LTL specifications are converted to safety automata via universal co-Buchi automata with a bound on final state visitations provided as a hyperparameter. Our application of CBBCs in verification is analogous: we fix a bound and search for a suitable barrier certificate, increasing the bound if no suitable function can be found. We then use these CBBCs to verify our system against properties specified by co-Buchi automata and demonstrate their effectiveness via some case studies.

cs.FL↗

arXiv2023

Closure Certificates

A barrier certificate, defined over the states of a dynamical system, is a real-valued function whose zero level set characterizes an inductively verifiable state invariant separating reachable states from unsafe ones. When combined with powerful decision procedures such as sum-of-squares programming (SOS) or satisfiability-modulo-theory solvers (SMT) barrier certificates enable an automated deductive verification approach to safety. The barrier certificate approach has been extended to refute omega-regular specifications by separating consecutive transitions of omega-automata in the hope of denying all accepting runs. Unsurprisingly, such tactics are bound to be conservative as refutation of recurrence properties requires reasoning about the well-foundedness of the transitive closure of the transition relation. This paper introduces the notion of closure certificates as a natural extension of barrier certificates from state invariants to transition invariants. We provide SOS and SMT based characterization for automating the search of closure certificates and demonstrate their effectiveness via a paradigmatic case study.

cs.LO↗

arXiv2022

Optimal Repair For Omega-regular Properties

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 $ω$-regular languages, and the repair space as repair machines -- weighted omega-regular transducers equipped with Büchi 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 $ω$-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.

cs.FL↗

arXiv2021

Verification of Hyperproperties for Uncertain Dynamical Systems via Barrier Certificates

Hyperproperties are system properties that require quantification over multiple execution traces of a system. Hyperproperties can express several specifications of interest for cyber-physical systems--such as opacity, robustness, and noninterference--which cannot be expressed using linear-time properties. This paper presents for the first time a discretization-free approach for the formal verification of discrete-time uncertain dynamical systems against hyperproperties. The proposed approach involves decomposition of complex hyperproperties into several verification conditions by exploiting the automata-based structures corresponding to the complements of the original specifications. These verification conditions are then discharged by synthesizing so-called augmented barrier certificates, which provide certain safety guarantees for the underlying system. For systems with polynomial-type dynamics, we present a sound procedure to synthesize polynomial-type augmented barrier certificates by reducing the problem to sum-of-squares optimizations. We demonstrate the effectiveness of our proposed approaches on two physical case studies against two important hyperproperties: initial-state opacity and initial-state robustness.

eess.SY↗