A Note on Runtime Verification of Concurrent Systems

• URL: http://arxiv.org/abs/2507.04830v1
• Date: Mon, 07 Jul 2025 09:50:59 GMT
• Title: A Note on Runtime Verification of Concurrent Systems
• Authors: Martin Leucker,
• Abstract summary: This paper offers an alternative perspective on verification of concurrent systems by leveraging trace-based logics.<n>The paper recalls a construction of trace-consistent B"uchi automata for LTrL formulas and explains how to employ it in well-understood monitor synthesis procedures.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: To maximize the information gained from a single execution when verifying a concurrent system, one can derive all concurrency-aware equivalent executions and check them against linear specifications. This paper offers an alternative perspective on verification of concurrent systems by leveraging trace-based logics rather than sequence-based formalisms. Linear Temporal Logic over Mazurkiewicz Traces (LTrL) operates on partial-order representations of executions, meaning that once a single execution is specified, all equivalent interleavings are implicitly considered. This paper introduces a three valued version of LTrL, indicating whether the so-far observed execution of the concurrent system is one of correct, incorrect or inconclusive, together with a suitable monitor synthesis procedure. To this end, the paper recalls a construction of trace-consistent B\"uchi automata for LTrL formulas and explains how to employ it in well-understood monitor synthesis procedures. In this way, a monitor results that yields for any linearization of an observed trace the same verification verdict.

Related papers

• SPARE: Single-Pass Annotation with Reference-Guided Evaluation for Automatic Process Supervision and Reward Modelling [70.01883340129204]
  Single-Pass.<n>with Reference-Guided Evaluation (SPARE)<n>Novel structured framework that enables single-pass, per-step annotation by aligning each solution step to one or multiple steps in a reference solution, accompanied by explicit reasoning for evaluation.<n>SPARE achieves competitive performance on challenging mathematical datasets while offering 2.6 times greater efficiency, requiring only 38% of the runtime.
  arXiv  Detail & Related papers  (2025-06-18T14:37:59Z)
• Execution Guided Line-by-Line Code Generation [49.1574468325115]
  We present a novel approach to neural code generation that incorporates real-time execution signals into the language model generation process.<n>Our method, ExecutionGuidedFree Guidance (EGCFG), incorporates execution signals as model generates code.
  arXiv  Detail & Related papers  (2025-06-12T17:50:05Z)
• Self-Calibrated Listwise Reranking with Large Language Models [137.6557607279876]
  Large language models (LLMs) have been employed in reranking tasks through a sequence-to-sequence approach. This reranking paradigm requires a sliding window strategy to iteratively handle larger candidate sets. We propose a novel self-calibrated listwise reranking method, which aims to leverage LLMs to produce global relevance scores for ranking.
  arXiv  Detail & Related papers  (2024-11-07T10:31:31Z)
• Runtime Instrumentation for Reactive Components (Extended Version) [0.0]
  Reactive software calls for instrumentation methods that uphold the reactive attributes of systems. This paper presents RIARC, a novel decentralised instrumentation algorithm for outline monitors meeting these two demands. RIARC overcomes these challenges using a next-hop IP routing approach to rearrange and report events soundly to monitors.
  arXiv  Detail & Related papers  (2024-06-28T13:18:04Z)
• Bisimulation Learning [55.859538562698496]
  We compute finite bisimulations of state transition systems with large, possibly infinite state space. Our technique yields faster verification results than alternative state-of-the-art tools in practice.
  arXiv  Detail & Related papers  (2024-05-24T17:11:27Z)
• Tooling Offline Runtime Verification against Interaction Models : recognizing sliced behaviors using parameterized simulation [0.4199844472131921]
  offline runtime verification involves the static analysis of executions of a system against a specification. For distributed systems, it is generally not possible to characterize executions in the form of global traces, given the absence of a global clock. We propose an algorithm that verifies the conformity of such traces against formal specifications called Interactions.
  arXiv  Detail & Related papers  (2024-03-05T16:09:55Z)
• Sound Concurrent Traces for Online Monitoring Technical Report [0.0]
  concurrent programs typically rely on collecting traces to abstract program executions. We first define the notion of when a trace is representative of a concurrent execution. We then present a non-blocking vector clock algorithm to collect sound concurrent traces on the fly.
  arXiv  Detail & Related papers  (2024-02-28T15:11:39Z)
• Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
  We consider the problem of automatically synthesizing formal specifications from system executions. Most of the classical approaches for synthesizing temporal logic formulas aim at minimizing the size of the formula. We formalize this notion and devise a learning algorithm that synthesizes concise formulas having bounded lookahead.
  arXiv  Detail & Related papers  (2023-10-26T14:13:15Z)
• Monitoring Algorithmic Fairness under Partial Observations [3.790015813774933]
  runtime verification techniques have been introduced to monitor the algorithmic fairness of deployed systems. Previous monitoring techniques assume full observability of the states of the monitored system. We extend fairness monitoring to systems modeled as partially observed Markov chains.
  arXiv  Detail & Related papers  (2023-08-01T07:35:54Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  This paper studies Linear Temporal Logic over Finite Traces (LTLf) proposition letters are replaced with first-order formulas interpreted over arbitrary theories. The resulting logic, called Satisfiability Modulo Theories (LTLfMT), is semi-decidable.
  arXiv  Detail & Related papers  (2022-04-28T17:57:33Z)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  We introduce the CoCoMoT (Computing Conformance Modulo Theories) framework. First, we show how SAT-based encodings studied in the pure control-flow setting can be lifted to our data-aware case. Second, we introduce a novel preprocessing technique based on a notion of property-preserving clustering.
  arXiv  Detail & Related papers  (2021-03-18T20:22:50Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.