arXiv subjects

Kim G. Larsen

Publications and source records attributed to Kim G. Larsen.

50 records · Page 3Linked to original sources

arXiv2012

Parameterized Metatheory for Continuous Markovian Logic

This paper shows that a classic metalogical framework, including all Boolean operators, can be used to support the development of a metric behavioural theory for Markov processes. Previously, only intuitionistic frameworks or frameworks without negation and logical implication have been developed to fulfill this task. The focus of this paper is on continuous Markovian logic (CML), a logic that characterizes stochastic bisimulation of Markov processes with an arbitrary measurable state space and continuous-time transitions. For a parameter epsilon>0 interpreted as observational error, we introduce an epsilon-parameterized metatheory for CML: we define the concepts of epsilon-satisfiability and epsilon-provability related by a sound and complete axiomatization and prove a series of "parameterized" metatheorems including decidability, weak completeness and finite model property. We also prove results regarding the relations between metalogical concepts defined for different parameters. Using this framework, we can characterize both the stochastic bisimulation relation and various observational preorders based on behavioural pseudometrics. The main contribution of this paper is proving that all these analyses can actually be done using a unified complete Boolean framework. This extends the state of the art in this field, since the related works only propose intuitionistic contexts that limit, for instance, the use of the Boolean logical implication.

cs.LO↗

arXiv2012

Learning Markov Decision Processes for Model Checking

Constructing an accurate system model for formal model verification can be both resource demanding and time-consuming. To alleviate this shortcoming, algorithms have been proposed for automatically learning system models based on observed system behaviors. In this paper we extend the algorithm on learning probabilistic automata to reactive systems, where the observed system behavior is in the form of alternating sequences of inputs and outputs. We propose an algorithm for automatically learning a deterministic labeled Markov decision process model from the observed behavior of a reactive system. The proposed learning algorithm is adapted from algorithms for learning deterministic probabilistic finite automata, and extended to include both probabilistic and nondeterministic transitions. The algorithm is empirically analyzed and evaluated by learning system models of slot machines. The evaluation is performed by analyzing the probabilistic linear temporal logic properties of the system as well as by analyzing the schedulers, in particular the optimal schedulers, induced by the learned models.

cs.LG↗

arXiv2012

Continuous Markovian Logics - Axiomatization and Quantified Metatheory

Continuous Markovian Logic (CML) is a multimodal logic that expresses quantitative and qualitative properties of continuous-time labelled Markov processes with arbitrary (analytic) state-spaces, henceforth called continuous Markov processes (CMPs). The modalities of CML evaluate the rates of the exponentially distributed random variables that characterize the duration of the labeled transitions of a CMP. In this paper we present weak and strong complete axiomatizations for CML and prove a series of metaproperties, including the finite model property and the construction of canonical models. CML characterizes stochastic bisimilarity and it supports the definition of a quantified extension of the satisfiability relation that measures the "compatibility" between a model and a property. In this context, the metaproperties allows us to prove two robustness theorems for the logic stating that one can perturb formulas and maintain "approximate satisfaction".

cs.LO↗

arXiv2012

Time-Darts: A Data Structure for Verification of Closed Timed Automata

Symbolic data structures for model checking timed systems have been subject to a significant research, with Difference Bound Matrices (DBMs) still being the preferred data structure in several mature verification tools. In comparison, discretization offers an easy alternative, with all operations having linear-time complexity in the number of clocks, and yet valid for a large class of closed systems. Unfortunately, fine-grained discretization causes itself a state-space explosion. We introduce a new data structure called time-darts for the symbolic representation of state-spaces of timed automata. Compared with the complete discretization, a single time-dart allows to represent an arbitrary large set of states, yet the time complexity of operations on time-darts remain linear in the number of clocks. We prove the correctness of the suggested reachability algorithm and perform several experiments in order to compare the performance of time-darts and the complete discretization. The main conclusion is that in all our experiments the time-dart method outperforms the complete discretization and it scales significantly better for models with larger constants.

cs.DS↗

arXiv2012

Weighted Modal Transition Systems

Specification theories as a tool in model-driven development processes of component-based software systems have recently attracted a considerable attention. Current specification theories are however qualitative in nature, and therefore fragile in the sense that the inevitable approximation of systems by models, combined with the fundamental unpredictability of hardware platforms, makes it difficult to transfer conclusions about the behavior, based on models, to the actual system. Hence this approach is arguably unsuited for modern software systems. We propose here the first specification theory which allows to capture quantitative aspects during the refinement and implementation process, thus leveraging the problems of the qualitative setting. Our proposed quantitative specification framework uses weighted modal transition systems as a formal model of specifications. These are labeled transition systems with the additional feature that they can model optional behavior which may or may not be implemented by the system. Satisfaction and refinement is lifted from the well-known qualitative to our quantitative setting, by introducing a notion of distances between weighted modal transition systems. We show that quantitative versions of parallel composition as well as quotient (the dual to parallel composition) inherit the properties from the Boolean setting.

cs.LO↗

arXiv2012

Statistical Model Checking for Stochastic Hybrid Systems

This paper presents novel extensions and applications of the UPPAAL-SMC model checker. The extensions allow for statistical model checking of stochastic hybrid systems. We show how our race-based stochastic semantics extends to networks of hybrid systems, and indicate the integration technique applied for implementing this semantics in the UPPAAL-SMC simulation engine. We report on two applications of the resulting tool-set coming from systems biology and energy aware buildings.

cs.CE↗

arXiv2012

On the Relationship between LTL Normal Forms and Buechi Automata

In this paper, we consider the problem of translating LTL formulas to Buechi automata. We first translate the given LTL formula into a special disjuctive-normal form (DNF). The formula will be part of the state, and its DNF normal form specifies the atomic properties that should hold immediately (labels of the transitions) and the formula that should hold afterwards (the corresponding successor state). Surprisingly, if the given formula is Until-free or Release-free, the Buechi automaton can be obtained directly in this manner. For a general formula, the construction is slightly involved: an additional component will be needed for each formula that helps us to identify the set of accepting states. Notably, our construction is an on-the-fly construction, and the resulting Buechi automaton has in worst case 2^{2n+1} states where n denotes the number of subformulas. Moreover, it has a better bound 2^{n+1} when the formula is Until- (or Release-) free.

cs.FL↗

arXiv2012

MDM: A Mode Diagram Modeling Framework for Periodic Control Systems

Periodic control systems used in spacecrafts and automotives are usually period-driven and can be decomposed into different modes with each mode representing a system state observed from outside. Such systems may also involve intensive computing in their modes. Despite the fact that such control systems are widely used in the above-mentioned safety-critical embedded domains, there is lack of domain-specific formal modelling languages for such systems in the relevant industry. To address this problem, we propose a formal visual modeling framework called MDM as a concise and precise way to specify and analyze such systems. To capture the temporal properties of periodic control systems, we provide, along with MDM, a property specification language based on interval logic for the description of concrete temporal requirements the engineers are concerned with. The statistical model checking technique can then be used to verify the MDM models against desired properties. To demonstrate the viability of our approach, we have applied our modelling framework to some real life case studies from industry and helped detect two design defects for some spacecraft control systems.

eess.SY↗

arXiv2012

Controllers with Minimal Observation Power (Application to Timed Systems)

We consider the problem of controller synthesis under imperfect information in a setting where there is a set of available observable predicates equipped with a cost function. The problem that we address is the computation of a subset of predicates sufficient for control and whose cost is minimal. Our solution avoids a full exploration of all possible subsets of predicates and reuses some information between different iterations. We apply our approach to timed systems. We have developed a tool prototype and analyze the performance of our optimization algorithm on two case studies.

eess.SY↗

arXiv2012

A "Hybrid" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example

In this paper, we propose an approach to reduce the optimal controller synthesis problem of hybrid systems to quantifier elimination; furthermore, we also show how to combine quantifier elimination with numerical computation in order to make it more scalable but at the same time, keep arising errors due to discretization manageable and within bounds. A major advantage of our approach is not only that it avoids errors due to numerical computation, but it also gives a better optimal controller. In order to illustrate our approach, we use the real industrial example of an oil pump provided by the German company HYDAC within the European project Quasimodo as a case study throughout this paper, and show that our method improves (up to 7.5%) the results reported in [3] based on game theory and model checking.

eess.SY↗

arXiv2012

Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach

This paper studies the problem of computing Nash equilibrium in wireless networks modeled by Weighted Timed Automata. Such formalism comes together with a logic that can be used to describe complex features such as timed energy constraints. Our contribution is a method for solving this problem using Statistical Model Checking. The method has been implemented in UPPAAL model checker and has been applied to the analysis of Aloha CSMA/CD and IEEE 802.15.4 CSMA/CA protocols.

cs.GT↗

arXiv2011

Distances for Weighted Transition Systems: Games and Properties

We develop a general framework for reasoning about distances between transition systems with quantitative information. Taking as starting point an arbitrary distance on system traces, we show how this leads to natural definitions of a linear and a branching distance on states of such a transition system. We show that our framework generalizes and unifies a large variety of previously considered system distances, and we develop some general properties of our distances. We also show that if the trace distance admits a recursive characterization, then the corresponding branching distance can be obtained as a least fixed point to a similar recursive characterization. The central tool in our work is a theory of infinite path-building games with quantitative objectives.

cs.LO↗

arXiv2010

On Zone-Based Analysis of Duration Probabilistic Automata

We propose an extension of the zone-based algorithmics for analyzing timed automata to handle systems where timing uncertainty is considered as probabilistic rather than set-theoretic. We study duration probabilistic automata (DPA), expressing multiple parallel processes admitting memoryfull continuously-distributed durations. For this model we develop an extension of the zone-based forward reachability algorithm whose successor operator is a density transformer, thus providing a solution to verification and performance evaluation problems concerning acyclic DPA (or the bounded-horizon behavior of cyclic DPA).

cs.FL↗

arXiv2008

Model Checking One-clock Priced Timed Automata

We consider the model of priced (a.k.a. weighted) timed automata, an extension of timed automata with cost information on both locations and transitions, and we study various model-checking problems for that model based on extensions of classical temporal logics with cost constraints on modalities. We prove that, under the assumption that the model has only one clock, model-checking this class of models against the logic WCTL, CTL with cost-constrained modalities, is PSPACE-complete (while it has been shown undecidable as soon as the model has three clocks). We also prove that model-checking WMTL, LTL with cost-constrained modalities, is decidable only if there is a single clock in the model and a single stopwatch cost variable (i.e., whose slopes lie in {0,1}).

cs.LO↗