arXiv subjects

Khushraj Madnani

Publications and source records attributed to Khushraj Madnani.

15 recordsLinked to original sources

arXiv2026

MightyPPL : Towards model checking MTL

The theoretical foundation for model checking timed systems against Metric Interval Temporal Logic (MITL) was established in the early 1990s, yet the first practical tool supporting future MITL (MightyL) did not emerge until 2017. Recently, there has been growing interest in extending this toolchain to support more expressive logical operators, including past modalities, Pnueli modalities, and limited use of singular intervals. MightyPPL is one such toolchain. We introduce an upgraded version of MIghtyPPL that enables for the first time, the model checking of Metric Temporal Logic (MTL) properties of the form (whenever an event p occurs, it is eventually followed by some event q after exactly some k time units) in addition to Pnueli and Past modalities. We discuss the tool's underlying architecture and implementation, and present a performance evaluation against the Tempora tool across diverse satisfiability and model checking benchmarks, demonstrating that MightyPPL delivers significantly better performance.

cs.LO↗

arXiv2026

On Synthesis of Metric Interval Temporal Logics

Automated mining of formal specifications is vital for verifying real-time systems. However, existing passive learning approaches remain restricted to deterministic specifications or limited fragments of Timed Regular Expressions (TRE). To our knowledge, this paper presents the first framework to tackle \emph{precise} passive learning for an expressive timed logic, \emph{Metric Interval Temporal Logic} (MITL) without relying on predefined templates or restricted logic fragments. Our approach formally reduces the timed learning problem into a scalable untimed one. By identifying quantitative timing differences between positive and negative traces, we synthesise precise timed constraints and inject them as new Boolean atomic propositions. This embeds timing into the alphabet, delegating the complex formula evaluation to highly optimised, off-the-shelf untimed LTL tools. Crucially, our framework is complete, guaranteeing a separating specification can always be found. We evaluate our implementation across several benchmarks, demonstrating the effectiveness of our approach.

cs.LO↗

arXiv2025

MightyPPL: Verification of MITL with Past and Pnueli Modalities

Metric Interval Temporal Logic (MITL) is a popular formalism for specifying properties of reactive systems with timing constraints. Existing approaches to using MITL in verification tasks, however, have notable drawbacks: they either support only limited fragments of the logic or allow for only incomplete verification. This paper introduces MightyPPL, a new tool for translating formulae in Metric Interval Temporal Logic with Past and Pnueli modalities (MITPPL) over the pointwise semantics into timed automata. MightyPPL enables satisfiability and model checking of a much more expressive specification logic over both finite and infinite words and incorporates a number of performance optimisations, including a novel symbolic encoding of transitions and a symmetry reduction technique that leads to an exponential improvement in the number of reachable discrete states. For a given MITPPL formula, MightyPPL can generate either a network of timed automata or a single timed automaton that is language-equivalent and compatible with multiple verification back-ends, including Uppaal, TChecker, and LTSmin, which supports multi-core model checking. We evaluate the performance of the toolchain across various case studies and configuration options.

cs.FL↗

arXiv2025

Approximate Problems for Finite Transducers

Finite (word) state transducers extend finite state automata by defining a binary relation over finite words, called rational relation. If the rational relation is the graph of a function, this function is said to be rational. The class of sequential functions is a strict subclass of rational functions, defined as the functions recognised by input-deterministic finite state transducers. The class membership problems between those classes are known to be decidable. We consider approximate versions of these problems and show they are decidable as well. This includes the approximate functionality problem, which asks whether given a rational relation (by a transducer), is it close to a rational function, and the approximate determinisation problem, which asks whether a given rational function is close to a sequential function. We prove decidability results for several classical distances, including Hamming and Levenshtein edit distance. Finally, we investigate the approximate uniformisation problem, which asks, given a rational relation $R$, whether there exists a sequential function that is close to some function uniformising $R$. As for its exact version, we prove that this problem is undecidable.

cs.FL↗

arXiv2024

Openness And Partial Adjacency In One Variable TPTL

Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) extend Linear Temporal Logic (LTL) for real-time constraints, with MTL using time-bounded modalities and TPTL employing freeze quantifiers. Satisfiability for both is generally undecidable; however, MTL becomes decidable under certain non-punctual and partially-punctual restrictions. Punctuality can be restored trivially under similar non-punctual restrictions on TPTL even for one variable fragment. Our first contribution is to study more restricted notion of openness for 1-TPTL, under which punctuality can not be recovered. We show that even under such restrictions, the satisfiability checking does not get computationally easier. This implies that 1-TPTL (and hence TPTL) does not enjoy benefits of relaxing punctuality unlike MTL. As our second contribution we introduce a refined, partially adjacent restriction in 1-TPTL (PA-1-TPTL), and prove decidability for its satisfiability checking. We show that this logic is strictly more expressive than partially punctual Metric Temporal Logic, making this as one of the most expressive known boolean-closed decidable timed logic.

cs.LO↗

arXiv2024

When Do You Start Counting? Revisiting Counting and Pnueli Modalities in Timed Logics

Pnueli first noticed that certain simple 'counting' properties appear to be inexpressible in popular timed temporal logics such as Metric Interval Temporal Logic (MITL). This interesting observation has since been studied extensively, culminating in strong timed logics that are capable of expressing such properties yet remain decidable. A slightly more general case, namely where one asserts the existence of a sequence of events in an arbitrary interval of the form (instead of an upper-bound interval of the form [0, b>, which starts from the current point in time), has however not been addressed satisfactorily in the existing literature. We show that counting in [0, b> is in fact as powerful as counting in ; moreover, the general property 'there exist x', x'' in I such that x' <= x'' and phi(x', x'') holds' can be expressed in Extended Metric Interval Temporal Logic (EMITL) with only [0, b>.

cs.LO↗

arXiv2024

An efficient quantifier elimination procedure for Presburger arithmetic

All known quantifier elimination procedures for Presburger arithmetic require doubly exponential time for eliminating a single block of existentially quantified variables. It has even been claimed in the literature that this upper bound is tight. We observe that this claim is incorrect and develop, as the main result of this paper, a quantifier elimination procedure eliminating a block of existentially quantified variables in singly exponential time. As corollaries, we can establish the precise complexity of numerous problems. Examples include deciding (i) monadic decomposability for existential formulas, (ii) whether an existential formula defines a well-quasi ordering or, more generally, (iii) certain formulas of Presburger arithmetic with Ramsey quantifiers. Moreover, despite the exponential blowup, our procedure shows that under mild assumptions, even NP upper bounds for decision problems about quantifier-free formulas can be transferred to existential formulas. The technical basis of our results is a kind of small model property for parametric integer programming that generalizes the seminal results by von zur Gathen and Sieveking on small integer points in convex polytopes.

cs.LO↗

arXiv2023

Monus semantics in vector addition systems with states

Vector addition systems with states (VASS) are a popular model for concurrent systems. However, many decision problems have prohibitively high complexity. Therefore, it is sometimes useful to consider overapproximating semantics in which these problems can be decided more efficiently. We study an overapproximation, called monus semantics, that slightly relaxes the semantics of decrements: A key property of a vector addition systems is that in order to decrement a counter, this counter must have a positive value. In contrast, our semantics allows decrements of zero-valued counters: If such a transition is executed, the counter just remains zero. It turns out that if only a subset of transitions is used with monus semantics (and the others with classical semantics), then reachability is undecidable. However, we show that if monus semantics is used throughout, reachability remains decidable. In particular, we show that reachability for VASS with monus semantics is as hard as that of classical VASS (i.e. Ackermann-hard), while the zero-reachability and coverability are easier (i.e. EXPSPACE-complete and NP-complete, respectively). We provide a comprehensive account of the complexity of the general reachability problem, reachability of zero configurations, and coverability under monus semantics. We study these problems in general VASS, two-dimensional VASS, and one-dimensional VASS, with unary and binary counter updates.

cs.LO↗

arXiv2021

Generalizing Non-Punctuality for Timed Temporal Logic with Freeze Quantifiers

Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are prominent real-time extensions of Linear Temporal Logic (LTL). In general, the satisfiability checking problem for these extensions is undecidable when both the future U and the past S modalities are used. In a classical result, the satisfiability checking for MITL[U,S], a non punctual fragment of MTL[U,S], is shown to be decidable with EXPSPACE complete complexity. Given that this notion of non punctuality does not recover decidability in the case of TPTL[U,S], we propose a generalization of non punctuality called \emph{non adjacency} for TPTL[U,S], and focus on its 1-variable fragment, 1-TPTL[U,S]. While non adjacent 1-TPTL[U,S] appears to be be a very small fragment, it is strictly more expressive than MITL. As our main result, we show that the satisfiability checking problem for non adjacent 1-TPTL[U,S] is decidable with EXPSPACE complete complexity.

cs.LO↗

arXiv2021

Self-Triggered Control for Near-Maximal Average Inter-Sample Time

Self-triggered control (STC) is a sample-and-hold control method aimed at reducing communications within networked-control systems; however, existing STC mechanisms often maximize how late the next sample is, and as such they do not provide any sampling optimality in the long-term. In this work, we devise a method to construct self-triggered policies that provide near-maximal average inter-sample time (AIST) while respecting given control performance constraints. To achieve this, we rely on finite-state abstractions of a reference event-triggered control, in which early triggers are also allowed. These early triggers constitute controllable actions of the abstraction, for which an AIST-maximizing strategy can be computed by solving a mean-payoff game. We provide optimality bounds, and how to further improve them through abstraction refinement techniques.

eess.SY↗

arXiv2018

Büchi-Kamp Theorems for 1-clock ATA

This paper investigates Kamp-like and Büchi-like theorems for 1-clock Alternating Timed Automata (1-ATA) and its natural subclasses. A notion of 1-ATA with loop-free-resets is defined. This automaton class is shown to be expressively equivalent to the temporal logic $\regmtl$ which is $\mathsf{MTL[F_I]}$ extended with a regular expression guarded modality. Moreover, a subclass of future timed MSO with k-variable-connectivity property is introduced as logic $\qkmso$. In a Kamp-like result, it is shown that $\regmtl$ is expressively equivalent to $\qkmso$. As our second result, we define a notion of conjunctive-disjunctive 1-clock ATA ($\wf$ 1-ATA). We show that $\wf$ 1-ATA with loop-free-resets are expressively equivalent to the sublogic $\F\regmtl$ of $\regmtl$. Moreover $\F\regmtl$ is expressively equivalent to $\qtwomso$, the two-variable connected fragment of $\qkmso$. The full class of 1-ATA is shown to be expressively equivalent to $\regmtl$ extended with fixed point operators.

cs.LO↗

arXiv2017

Making Metric Temporal Logic Rational

We study an extension of $\mtl$ in pointwise time with rational expression guarded modality $\reg_I(\re)$ where $\re$ is a rational expression over subformulae. We study the decidability and expressiveness of this extension ($\mtl$+$φ\ureg_{I, \re} φ$+$\reg_{I,\re}φ$), called $\regmtl$, as well as its fragment $\sfmtl$ where only star-free rational expressions are allowed. Using the technique of temporal projections, we show that $\regmtl$ has decidable satisfiability by giving an equisatisfiable reduction to $\mtl$. We also identify a subclass $\mitl+\ureg$ of $\regmtl$ for which our equi-satisfiable reduction gives rise to formulae of $\mitl$, yielding elementary decidability. As our second main result, we show a tight automaton-logic connection between $\sfmtl$ and partially ordered (or very weak) 1-clock alternating timed automata.

cs.LO↗

arXiv2015

Metric Temporal Logic with Counting

Ability to count number of occurrences of events within a specified time interval is very useful in specification of resource bounded real time computation. In this paper, we study an extension of Metric Temporal Logic ($\mathsf{MTL}$) with two different counting modalities called $\mathsf{C}$ and $\mathsf{UT}$ (until with threshold), which enhance the expressive power of $\mathsf{MTL}$ in orthogonal fashion. We confine ourselves only to the future fragment of $\mathsf{MTL}$ interpreted in a pointwise manner over finite timed words. We provide a comprehensive study of the expressive power of logic $\mathsf{CTMTL}$ and its fragments using the technique of EF games extended with suitable counting moves. Finally, as our main result, we establish the decidability of $\mathsf{CTMTL}$ by giving an equisatisfiable reduction from $\mathsf{CTMTL}$ to $\mathsf{MTL}$. The reduction provides one more example of the use of temporal projections with oversampling introduced earlier for proving decidability. Our reduction also implies that $\mathsf{MITL}$ extended with $\mathsf{C}$ and $\mathsf{UT}$ modalities is elementarily decidable.

cs.LO↗

arXiv2014

Partially Punctual Metric Temporal Logic is Decidable

Metric Temporal Logic $\mathsf{MTL}[\until_I,\since_I]$ is one of the most studied real time logics. It exhibits considerable diversity in expressiveness and decidability properties based on the permitted set of modalities and the nature of time interval constraints $I$. Henzinger et al., in their seminal paper showed that the non-punctual fragment of $\mathsf{MTL}$ called $\mathsf{MITL}$ is decidable. In this paper, we sharpen this decidability result by showing that the partially punctual fragment of $\mathsf{MTL}$ (denoted $\mathsf{PMTL}$) is decidable over strictly monotonic finite point wise time. In this fragment, we allow either punctual future modalities, or punctual past modalities, but never both together. We give two satisfiability preserving reductions from $\mathsf{PMTL}$ to the decidable logic $\mathsf{MTL}[\until_I]$. The first reduction uses simple projections, while the second reduction uses a novel technique of temporal projections with oversampling. We study the trade-off between the two reductions: while the second reduction allows the introduction of extra action points in the underlying model, the equisatisfiable $\mathsf{MTL}[\until_I]$ formula obtained is exponentially succinct than the one obtained via the first reduction, where no oversampling of the underlying model is needed. We also show that $\mathsf{PMTL}$ is strictly more expressive than the fragments $\mathsf{MTL}[\until_I,\since]$ and $\mathsf{MTL}[\until,\since_I]$.

cs.LO↗

arXiv2013

On the Decidability and Complexity of Some Fragments of Metric Temporal Logic

Metric Temporal Logic, $\mtlfull$ is amongst the most studied real-time logics. It exhibits considerable diversity in expressiveness and decidability properties based on the permitted set of modalities and the nature of time interval constraints $I$. \oomit{The classical results of Alur and Henzinger showed that $\mtlfull$ is undecidable where as $\mitl$ which uses only non-singular intervals $NS$ is decidable. In a surprizing result, Ouaknine and Worrell showed that the satisfiability of $\mtl$ is decidable over finite pointwise models, albeit with NPR decision complexity, whereas it remains undecidable for infinite pointwise models or for continuous time.} In this paper, we sharpen the decidability results by showing that the satisfiability of $\mtlsns$ (where $NS$ denotes non-singular intervals) is also decidable over finite pointwise strictly monotonic time. We give a satisfiability preserving reduction from the logic $\mtlsns$ to decidable logic $\mtl$ of Ouaknine and Worrell using the technique of temporal projections. We also investigate the decidability of unary fragment $\mtlfullunary$ (a question posed by A. Rabinovich) and show that $\mtlfut$ over continuous time as well as $\mtlfullunary$ over finite pointwise time are both undecidable. Moreover, $\mathsf{MTL}^{pw}[\fut_I]$ over finite pointwise models already has NPR lower bound for satisfiability checking. We also compare the expressive powers of some of these fragments using the technique of EF games for $\mathsf{MTL}$.

cs.LO↗