Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 1309.5151

Model Checking in Bits and Pieces

Kedar S. Namjoshi
View original source ↗Read source document ↗Export metadata ↓

Abstract

Fully automated verification of concurrent programs is a difficult problem, primarily because of state explosion: the exponential growth of a program state space with the number of its concurrently active components. It is natural to apply a divide and conquer strategy to ameliorate state explosion, by analyzing only a single component at a time. We show that this strategy leads to the notion of a "split" invariant, an assertion which is globally inductive, while being structured as the conjunction of a number of local, per-component invariants. This formulation is closely connected to the classical Owicki-Gries method and to Rely-Guarantee reasoning. We show how the division of an invariant into a number of pieces with limited scope makes it possible to apply new, localized forms of symmetry and abstraction to drastically simplify its computation. Split invariance also has interesting connections to parametric verification. A quantified invariant for a parametric system is a split invariant for every instance. We show how it is possible, in some cases, to invert this connection, and to automatically generalize from a split invariant for a small instance of a system to a quantified invariant which holds for the entire family of instances.

Explore related subjects

cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Kedar S. Namjoshi. 2013-09-20. Model Checking in Bits and Pieces. https://doi.org/10.4204/eptcs.129.25

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

The Complexity of Generalized HyperLTL with Stuttering and Contexts

We settle the complexity of satisfiability, finite-state satisfiability, and model-checking for generalized HyperLTL with stuttering and contexts, an expressive logic for the specification of asynchronous hyperproperties. Such properties cannot be specified in HyperLTL, as it is restricted to synchronous hyperproperties. Nevertheless, we prove that satisfiability is $Σ_1^1$-complete and thus not harder than for HyperLTL. On the other hand, we prove that model-checking and finite-state satisfiability are equivalent to truth in second-order arithmetic, and thus much harder than the decidable HyperLTL model-checking problem and the $Σ_0^1$-complete HyperLTL finite-state satisfiability problem. The lower bounds for the model-checking and finite-state satisfiability problems hold even when only allowing stuttering or only allowing contexts.

cs.LO↗
arXiv2026

STLSat---An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas

Signal Temporal Logic (STL) is a formalism used to describe temporal properties of real-valued signals in cyber-physical systems. In mission- and safety-critical domains, specifications often consist of large collections of STL formulas, making consistency checking and requirement analysis a major engineering bottleneck. Tableau-based satisfiability procedures are a natural way to address this problem. Two of the authors of this paper contributed to the only existing tree-shaped tableau for bounded discrete-time STL, but we have recently found out that the procedure can return incorrect verdicts for some STL formulas. In this paper, we pinpoint the flaw in that procedure and present a new tree-shaped tableau that we prove to be sound and complete for bounded discrete-time STL. On top of this theoretical foundation, we introduce STLSat, an open-source Rust tool that decides the satisfiability of STL formulas, synthesizes concrete witness signals, and extracts unsatisfiable cores with its tableau engine, allowing users to identify inconsistent subsets of requirements for more effective specification debugging. STLSat also implements enhanced first-order logic and satisfiability modulo theories encodings for STL, which allow it to act as a portfolio solver. We evaluate STLSat on an extended benchmark suite (including STL and Mission-time Linear Temporal Logic formulas) that we release publicly. Across the whole benchmark, the portfolio solver matches or outperforms state-of-the-art tools while preserving correctness.

cs.LO↗
arXiv2026

Adaptive Strategies for GR(1) Games

We consider two-player GR(1) games on graphs, where the system player Eve must satisfy \[ \Box\Diamond A_1\land\cdots\land\Box\Diamond A_m \;\implies\; \Box\Diamond G_1\land\cdots\land\Box\Diamond G_n \] against the environment player Adam. Here $A_1,\ldots,A_m$ are assumptions on the environment, $G_1,\ldots,G_n$ are guarantees the system must provide, and $\Box\Diamond S$ denotes ``always eventually $S$''. Traditional static strategies are overly conservative: they may actively violate assumptions to trivially satisfy the implication, or abandon all guarantees when any assumption is violated. Existing methods to prevent such behaviors incur doubly exponential blowup. We introduce an adaptive framework treating Adam as a non-adversarial agent with unknown objectives. Eve monitors which assumptions Adam actually meets and adapts her strategy at runtime to maximize satisfied guarantees. Central to our approach is a novel algorithm for monitoring liveness properties $\Box\Diamond S$, enabling Eve to maintain real-time likelihood estimates of which assumptions will be fulfilled. Eve pre-computes strategies optimal for different assumption subsets, deploying a probability distribution over them that dynamically adjusts based on monitor outputs. We prove that when assumptions are violated, Eve's randomized adaptive strategy converges asymptotically to the deterministic strategy maximizing guarantees. A prototype demonstrates effectiveness and superior computational performance compared to the state of the art.

cs.LO↗