首页/论文/2007.04150

arXiv 2007.041502020-07-08cs.LOcs.FL

Certifying Emptiness of Timed Büchi Automata

Simon Wimmer, Frédéric Herbreteau, Jaco van de Pol

备注：: A shorter version appears in the proceedings of FORMATS 2020

英文摘要：

Model checkers for timed automata are widely used to verify safety-critical, real-time systems. State-of-the-art tools achieve scalability by intricate abstractions. We aim at further increasing the trust in their verification results, in particular for checking liveness properties. To this end, we develop an approach for extracting certificates for the emptiness of timed Büchi automata from model checking runs. These certificates can be double-checked by a certifier that we formally verify in Isabelle/HOL. We study liveness certificates in an abstract setting and show that our approach is sound and complete. To also demonstrate its feasibility, we extract certificates for several models checked by TChecker and Imitator, and validate them with our verified certifier.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

Efficient Emptiness Check for Timed Büchi Automata (Extended version)

The Büchi non-emptiness problem for timed automata refers to deciding if a given automaton has an infinite non-Zeno run satisfying the Büchi accepting condition. The standard solution to this problem involves adding an auxiliary clock to take care of the non-Zenoness. In this paper, it is shown that this simple transformation may sometimes result in an exponential blowup. A construction avoiding this blowup is proposed. It is also shown that in many cases, non-Zenoness can be ascertained without extra construction. An on-the-fly algorithm for the non-emptiness problem, using non-Zenoness const…

2020-12-04cs.LO

Logics Meet 2-Way 1-Clock Alternating Timed Automata

In this paper, we study the extension of 1-clock Alternating Timed Automata (1-ATA) with the ability to read in both forward and backward direction, the 2-Way 1-clock Alternating Timed Automata (2-Way 1-ATA). We show that subclass of 2-Way 1-ATA with reset free loops (2-Way 1-ATA-rfl) is expressively equivalent to MSO[<] extended with Guarded Metric Quantifiers (GQMSO). Emptiness Checking problem for 2-Way 1-ATA-rfl (and hence GQMSO) is undecidable, in general. We propose a "non-punctuality" like restriction, called non-adjacency, for 2-Way 1-ATA-rfl, and also for GQMSO, for which the emptines…

2022-02-26cs.FLcs.LO

Alternating Timed Automata

A notion of alternating timed automata is proposed. It is shown that such automata with only one clock have decidable emptiness problem over finite words. This gives a new class of timed languages which is closed under boolean operations and which has an effective presentation. We prove that the complexity of the emptiness problem for alternating timed automata with one clock is non-primitive recursive. The proof gives also the same lower bound for the universality problem for nondeterministic timed automata with one clock. We investigate extension of the model with epsilon-transitions and pro…

2006-08-24cs.LO

Towards an Efficient Tree Automata based technique for Timed Systems

The focus of this paper is the analysis of real-time systems with recursion, through the development of good theoretical techniques which are implementable. Time is modeled using clock variables, and recursion using stacks. Our technique consists of modeling the behaviours of the timed system as graphs, and interpreting these graphs on tree terms by showing a bound on their tree-width. We then build a tree automaton that accepts exactly those tree terms that describe realizable runs of the timed system. The emptiness of the timed system thus boils down to emptiness of a finite tree automaton t…

2017-07-08cs.FLcs.LO

对实时系统的模型检验：重新审视交替自动机路线

Model-checking real-time systems: revisiting the alternating automaton route

本文提出了一种基于区域方法的1-ATA空性算法，改进了MTL到1-ATA的转换，并研究了在特定条件下模型检验实时系统的方法。

2026-01-06cs.FLcs.LO

Timed pushdown automata revisited

This paper contains two results on timed extensions of pushdown automata (PDA). As our first result we prove that the model of dense-timed PDA of Abdulla et al. collapses: it is expressively equivalent to dense-timed PDA with timeless stack. Motivated by this result, we advocate the framework of first-order definable PDA, a specialization of PDA in sets with atoms, as the right setting to define and investigate timed extensions of PDA. The general model obtained in this way is Turing complete. As our second result we prove NEXPTIME upper complexity bound for the non-emptiness problem for an ex…

2015-04-17cs.FLcs.LO

更多相关论文收起更多论文

MTL-Model Checking of One-Clock Parametric Timed Automata is Undecidable

Parametric timed automata extend timed automata (Alur and Dill, 1991) in that they allow the specification of parametric bounds on the clock values. Since their introduction in 1993 by Alur, Henzinger, and Vardi, it is known that the emptiness problem for parametric timed automata with one clock is decidable, whereas it is undecidable if the automaton uses three or more parametric clocks. The problem is open for parametric timed automata with two parametric clocks. Metric temporal logic, MTL for short, is a widely used specification language for real-time systems. MTL-model checking of timed a…

2014-04-01cs.FLcs.LO

On The Reachability Problem for Recursive Hybrid Automata with One and Two Players

Motivated by the success of bounded model checking framework for finite state machines, Ouaknine and Worrell proposed a time-bounded theory of real-time verification by claiming that restriction to bounded-time recovers decidability for several key decision problem related to real-time verification. In support of this theory, the list of undecidable problems recently shown decidable under time-bounded restriction is rather impressive: language inclusion for timed automata, emptiness problem for alternating timed automata, and emptiness problem for rectangular hybrid automata. The objective of …

2014-08-15cs.FLcs.LO

Weak Alternating Timed Automata

Alternating timed automata on infinite words are considered. The main result is a characterization of acceptance conditions for which the emptiness problem for these automata is decidable. This result implies new decidability results for fragments of timed temporal logics. It is also shown that, unlike for MITL, the characterisation remains the same even if no punctual constraints are allowed.

2012-09-16cs.LO

A Note on Fault Diagnosis Algorithms

In this paper we review algorithms for checking diagnosability of discrete-event systems and timed automata. We point out that the diagnosability problems in both cases reduce to the emptiness problem for (timed) Büchi automata. Moreover, it is known that, checking whether a discrete-event system is diagnosable, can also be reduced to checking bounded diagnosability. We establish a similar result for timed automata. We also provide a synthesis of the complexity results for the different fault diagnosis problems.

2010-04-16cs.FLcs.LO

Relating timed and register automata

Timed automata and register automata are well-known models of computation over timed and data words respectively. The former has clocks that allow to test the lapse of time between two events, whilst the latter includes registers that can store data values for later comparison. Although these two models behave in appearance differently, several decision problems have the same (un)decidability and complexity results for both models. As a prominent example, emptiness is decidable for alternating automata with one clock or register, both with non-primitive recursive complexity. This is not by cha…

2010-11-30cs.FLcs.LO

参数化时间自动机中的可达性与活性

Reachability and liveness in parametric timed automata

本文研究参数化时间自动机（PTAs）的可达性与活性，通过提出整数点PTAs子类推进可判定性边界，并证明L/U-PTAs中无限运行存在性为PSpace完全，而死锁存在性不可判定。

2022-02-07cs.LO

密集整数完备合成 for 有界参数时序自动机

Dense Integer-Complete Synthesis for Bounded Parametric Timed Automata

Université Sorbonne Paris Nord（索邦巴黎北大学）；Institut Universitaire de France (IUF)（法国大学研究院）；Nantes Université, École Centrale Nantes, CNRS, LS2N（南特大学，中央理工-南特学院，法国国家科学研究中心，LS2N）

本文提出了一种参数外推方法，用于在有界参数域内合成参数估值集，确保可达性和无避免性，同时保持与参考估值的无时行为。

2026-04-27cs.LO

Event-Clock Automata: From Theory to Practice

Event clock automata (ECA) are a model for timed languages that has been introduced by Alur, Fix and Henzinger as an alternative to timed automata, with better theoretical properties (for instance, ECA are determinizable while timed automata are not). In this paper, we revisit and extend the theory of ECA. We first prove that no finite time abstract language equivalence exists for ECA, thereby disproving a claim in the original work on ECA. This means in particular that regions do not form a time abstract bisimulation. Nevertheless, we show that regions can still be used to build a finite auto…

2011-07-22cs.LO

多变量单侧区间TPTL的可满足性检验是PSPACE完全的

Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete

IIT Bombay（印度理工学院孟买分校）；MPI-SWS（马克斯·普朗克软件系统研究所）

本文证明多变量单侧区间TPTL的可满足性检验为PSPACE完全，且其表达力严格强于MITL，但检验复杂度更低，通过归约到新的非点式交替定时自动机子类实现。

2023-09-01cs.CLcs.FLcs.LO