相关论文: Real-Time Model-Checking: Parameters everywhere

Linear Temporal Logic (LTL) is a widely used specification framework for linear time properties of systems. The standard approach for verifying such properties is by transforming LTL formulae to suitable $\omega$-automata and then applying…

This paper explores the theoretical limits of using discrete abstractions for nonlinear control synthesis. More specifically, we consider the problem of deciding continuous-time control with temporal logic specifications. We prove that…

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…

Verification of temporal logic properties plays a crucial role in proving the desired behaviors of continuous systems. In this paper, we propose an interval method that verifies the properties described by a bounded signal temporal logic.…

We consider quantitative extensions of the alternating-time temporal logics ATL/ATLs called quantitative alternating-time temporal logics (QATL/QATLs) in which the value of a counter can be compared to constants using equality, inequality…

Quantitative extensions of temporal logics have recently attracted significant attention. In this work, we study frequency LTL (fLTL), an extension of LTL which allows to speak about frequencies of events along an execution. Such an…

Recently there has been a great attention from the scientific community towards the use of the model-checking technique as a tool for test generation in the simulation field. This paper aims to provide a useful mean to get more insights…

We discuss the problem of experimentally evaluating linear-time temporal logic (LTL) synthesis tools for reactive systems. We first survey previous such work for the currently publicly available synthesis tools, and then draw conclusions by…

It is well known that the verification of resource-constrained multiagent systems is undecidable in general. In many such settings, resources are private to agents. In this paper, we investigate the model checking problem for a resource…

Linear temporal logic (LTL) is a specification language for finite sequences (called traces) widely used in program verification, motion planning in robotics, process mining, and many other areas. We consider the problem of learning LTL…

We consider distributed systems with an arbitrary number of processes, modelled by timed automata that communicate through location guards: a process can take a guarded transition if at least one other process is in a given location. In…

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…

In this paper we extend the predicate logic introduced in [Beauquier et al. 2002] in order to deal with Semi-Markov Processes. We prove that with respect to qualitative probabilistic properties, model checking is decidable for this logic…

The paper is focused on temporal logics for the description of the behaviour of real-time pushdown reactive systems. The paper is motivated to bridge tractable logics specialized for expressing separately dense-time real-time properties and…

One of the advantages of adopting a Model Based Development (MBD) process is that it enables testing and verification at early stages of development. However, it is often desirable to not only verify/falsify certain formal system…

Timing information leakage occurs whenever an attacker successfully deduces confidential internal information by observing some timed information such as events with timestamps. Timed automata are an extension of finite-state automata with…

Synthesis of models and strategies is a very important problem in software engineering. The main element here is checking the satisfiability of formulae expressing the specification of a system to be implemented. This paper puts forward a…

Parametric analysis is a powerful tool for designing modern embedded systems, because it permits to explore the space of design parameters, and to check the robustness of the system with respect to variations of some uncontrollable…

Hyperproperties are properties of computational systems that require more than one trace to evaluate, e.g., many information-flow security and concurrency requirements. Where a trace property defines a set of traces, a hyperproperty defines…

Probabilistic models often have parameters that can be translated, scaled, permuted, or otherwise transformed without changing the model. These symmetries can lead to strong correlation and multimodality in the posterior distribution over…