BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Javier Esparza

Javier Esparza appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
Logic in Computer ScienceFormal Languages and Automata TheoryDistributed, Parallel, and Cluster ComputingData Structures and AlgorithmsNumerical AnalysisComputational ComplexityMultiagent SystemsPerformanceProgramming Languages

Catalog footprint

What is connected

30works
9topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

30 published item(s)

preprint2022arXiv

Lower Bounds on the State Complexity of Population Protocols

Population protocols are a model of computation in which an arbitrary number of indistinguishable finite-state agents interact in pairs. The goal of the agents is to decide by stable consensus whether their initial global configuration satisfies a given property, specified as a predicate on the set of configurations. The state complexity of a predicate is the number of states of a smallest protocol that computes it. Previous work by Blondin \textit{et al.} has shown that the counting predicates $x \geq η$ have state complexity $\mathcal{O}(\log η)$ for leaderless protocols and $\mathcal{O}(\log \log η)$ for protocols with leaders. We obtain the first non-trivial lower bounds: the state complexity of $x \geq η$ is $Ω(\log\log η)$ for leaderless protocols, and the inverse of a non-elementary function for protocols with leaders.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

The Complexity of Verifying Population Protocols

Population protocols [Angluin et al., PODC, 2004] are a model of distributed computation in which indistinguishable, finite-state agents interact in pairs to decide if their initial configuration, i.e., the initial number of agents in each state, satisfies a given property. In a seminal paper Angluin et al. classified population protocols according to their communication mechanism, and conducted an exhaustive study of the expressive power of each class, that is, of the properties they can decide [Angluin et al., Distributed Computing, 2007]. In this paper we study the correctness problem for population protocols, i.e., whether a given protocol decides a given property. A previous paper [Esparza et al., Acta Informatica, 2017] has shown that the problem is decidable for the main population protocol model, but at least as hard as the reachability problem for Petri nets, which has recently been proved to have non-elementary complexity. Motivated by this result, we study the computational complexity of the correctness problem for all other classes introduced by Angluin et al., some of which are less powerful than the main model. Our main results show that for the class of observation models the complexity of the problem is much lower, ranging from $Π_2^p$ to PSPACE.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

A Classification of Weak Asynchronous Models of Distributed Computing

We conduct a systematic study of asynchronous models of distributed computing consisting of identical finite-state devices that cooperate in a network to decide if the network satisfies a given graph-theoretical property. Models discussed in the literature differ in the detection capabilities of the agents residing at the nodes of the network (detecting the set of states of their neighbors, or counting the number of neighbors in each state), the notion of acceptance (acceptance by halting in a particular configuration, or by stable consensus), the notion of step (synchronous move, interleaving, or arbitrary timing), and the fairness assumptions (non-starving, or stochastic-like). We study the expressive power of the combinations of these features, and show that the initially twenty possible combinations fit into seven equivalence classes. The classification is the consequence of several equi-expressivity results with a clear interpretation. In particular, we show that acceptance by halting configuration only has non-trivial expressive power if it is combined with counting, and that synchronous and interleaving models have the same power as those in which an arbitrary set of nodes can move at the same time. We also identify simple graph properties that distinguish the expressive power of the seven classes.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata

In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form $\bigwedge_{i=1}^n \mathbf{G}\mathbf{F} φ_i \vee \mathbf{F}\mathbf{G} ψ_i$, where $φ_i$ and $ψ_i$ contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. Both normalisation procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. We improve on both points. We present a direct and purely syntactic normalisation procedure for LTL yielding a normal form, comparable to the one by Chang, Manna, and Pnueli, that has only a single exponential blow-up. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalises the formula, translates it into a special very weak alternating automaton, and applies a simple determinisation procedure, valid only for these special automata.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling

We present a sound and complete method for the verification of qualitative liveness properties of replicated systems under stochastic scheduling. These are systems consisting of a finite-state program, executed by an unknown number of indistinguishable agents, where the next agent to make a move is determined by the result of a random experiment. We show that if a property of such a system holds, then there is always a witness in the shape of a Presburger stage graph: a finite graph whose nodes are Presburger-definable sets of configurations. Due to the high complexity of the verification problem (non-elementary), we introduce an incomplete procedure for the construction of Presburger stage graphs, and implement it on top of an SMT solver. The procedure makes extensive use of the theory of well-quasi-orders, and of the structural theory of Petri nets and vector addition systems. We apply our results to a set of benchmarks, in particular to a large collection of population protocols, a model of distributed computation extensively studied by the distributed computing community.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Flatness and Complexity of Immediate Observation Petri Nets

In a previous paper we introduced immediate observation (IO) Petri nets, a class of interest in the study of population protocols and enzymatic chemical networks. In the first part of this paper we show that IO nets are globally flat, and so their safety properties can be checked by efficient symbolic model checking tools using acceleration techniques, like FAST. In the second part we study Branching IO nets (BIO nets), whose transitions can create tokens. BIO nets extend both IO nets and communication-free nets, also called BPP nets, a widely studied class. We show that, while BIO nets are no longer globally flat, and their sets of reachable markings may be non-semilinear, they are still locally flat. As a consequence, the coverability and reachability problem for BIO nets, and even a certain set-parameterized version of them, are in PSPACE. This makes BIO nets the first natural net class with non-semilinear reachability relation for which the reachability problem is provably simpler than for general Petri nets.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Online Monitoring $ω$-Regular Properties in Unknown Markov Chains

We study runtime monitoring of $ω$-regular properties. We consider a simple setting in which a run of an unknown finite-state Markov chain $\mathcal M$ is monitored against a fixed but arbitrary $ω$-regular specification $φ$. The purpose of monitoring is to keep aborting runs that are "unlikely" to satisfy the specification until $\mathcal M$ executes a correct run. We design controllers for the reset action that (assuming that $φ$ has positive probability) satisfy the following property w.p.1: the number of resets is finite, and the run executed by $\mathcal M$ after the last reset satisfies $φ$.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Peregrine 2.0: Explaining Correctness of Population Protocols through Stage Graphs

We present a new version of Peregrine, the tool for the analysis and parameterized verification of population protocols introduced in [Blondin et al., CAV'2018]. Population protocols are a model of computation, intensely studied by the distributed computing community, in which mobile anonymous agents interact stochastically to perform a task. Peregrine 2.0 features a novel verification engine based on the construction of stage graphs. Stage graphs are proof certificates, introduced in [Blondin et al., CAV'2020], that are typically succinct and can be independently checked. Moreover, unlike the techniques of Peregrine 1.0, the stage graph methodology can verify protocols whose executions never terminate, a class including recent fast majority protocols. Peregrine 2.0 also features a novel proof visualization component that allows the user to interactively explore the stage graph generated for a given protocol.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Succinct Population Protocols for Presburger Arithmetic

Angluin et al. proved that population protocols compute exactly the predicates definable in Presburger arithmetic (PA), the first-order theory of addition. As part of this result, they presented a procedure that translates any formula $φ$ of quantifier-free PA with remainder predicates (which has the same expressive power as full PA) into a population protocol with $2^{O(\text{poly}(|φ|))}$ states that computes $φ$. More precisely, the number of states of the protocol is exponential in both the bit length of the largest coefficient in the formula, and the number of nodes of its syntax tree. In this paper, we prove that every formula $φ$ of quantifier-free PA with remainder predicates is computable by a leaderless population protocol with $O(\text{poly}(|φ|))$ states. Our proof is based on several new constructions, which may be of independent interest. Given a formula $φ$ of quantifier-free PA with remainder predicates, a first construction produces a succinct protocol (with $O(|φ|^3)$ leaders) that computes $φ$; this completes the work initiated in [STACS'18], where we constructed such protocols for a fragment of PA. For large enough inputs, we can get rid of these leaders. If the input is not large enough, then it is small, and we design another construction producing a succinct protocol with one leader that computes $φ$. Our last construction gets rid of this leader for small inputs.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Negotiation as Concurrency Primitive

This paper introduces negotiations, a model of concurrency close to Petri nets, with multi-party negotiations as concurrency primitive. We study two fundamental analysis problems. The soundness problem consists in deciding if it is always possible for a negotiation to terminate successfully, whatever the current state is. Given a sound negotiation, the summarization problem aims at computing an equivalent one-step negotiation with the same input/output behavior. The soundness and summarization problems can be solved by means of simple algorithms acting on the state space of the negotiation, which however face the well-known state explosion problem. We study alternative algorithms that avoid the construction of the state space. In particular, we define reduction rules that simplify a negotiation while preserving the sound/non-sound character of the negotiation and its summary. In a first result we show that our rules are complete for the class of weakly deterministic acyclic negotiations, meaning that they reduce all sound negotiations in this class, and only them, to equivalent one-step negotiations. This provides algorithms for both the soundness and summarization problems that avoid the construction of the state space. We then study the class of deterministic negotiations. Our second main result shows that the rules are also complete for this class, even if the negotiation contains cycles. Moreover, we present an algorithm that completely reduces all sound deterministic negotiations, and only them, in polynomial time.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

On Negotiation as Concurrency Primitive II: Deterministic Cyclic Negotiations

We continue our study of negotations, a concurrency model with multiparty negotiation as primitive. In a previous paper (arXiv:13072145) we have provided a correct and complete set of reduction rules for sound, acyclic, and (weakly) deterministic negotiations. In this paper we extend this result to all deterministic negotiations, including cyclic ones. We also show that this set of rules allows one to decide soundness and to summarize negotiations in polynomial time.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Polynomial Analysis Algorithms for Free Choice Probabilistic Workflow Nets

We study Probabilistic Workflow Nets (PWNs), a model extending van der Aalst's workflow nets with probabilities. We give a semantics for PWNs in terms of Markov Decision Processes and introduce a reward model. Using a result by Varacca and Nielsen, we show that the expected reward of a complete execution of the PWN is independent of the scheduler. Extending previous work on reduction of non-probabilistic workflow nets, we present reduction rules that preserve the expected reward. The rules lead to a polynomial-time algorithm in the size of the PWN (not of the Markov decision process) for the computation of the expected reward. In contrast, since the Markov decision process of PWN can be exponentially larger than the PWN itself, all algorithms based on constructing the Markov decision process require exponential time. We report on a sample implementation and its performance on a collection of benchmarks.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Reduction Rules for Colored Workflow Nets

We study Colored Workflow nets, a model based on Workflow nets enriched with data. Based on earlier work by Esparza and Desel[arXiv:1307.2145,arXiv:1403.4958] on the negotiation model of concurrency, we present reduction rules for our model. Contrary to previous work, our rules preserve not only soundness, but also the data flow semantics. For free choice nets, the rules reduce all sound nets (and only them) to a net with one single transition and the same data flow semantics. We give an explicit algorithm that requires only a polynomial number of rule applications.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Model Checking Parameterized Asynchronous Shared-Memory Systems

We characterize the complexity of liveness verification for parameterized systems consisting of a leader process and arbitrarily many anonymous and identical contributor processes. Processes communicate through a shared, bounded-value register. While each operation on the register is atomic, there is no synchronization primitive to execute a sequence of operations atomically. We analyze the case in which processes are modeled by finite-state machines or pushdown machines and the property is given by a Büchi automaton over the alphabet of read and write actions of the leader. We show that the problem is decidable, and has a surprisingly low complexity: it is NP-complete when all processes are finite-state machines, and is PSPACE-hard and in NEXPTIME when they are pushdown machines. This complexity is lower than for the non-parameterized case: liveness verification of finitely many finite-state machines is PSPACE-complete, and undecidable for two pushdown machines. For finite-state machines, our proofs characterize infinite behaviors using existential abstraction and semilinear constraints. For pushdown machines, we show how contributor computations of high stack height can be simulated by computations of many contributors, each with low stack height. Together, our results characterize the complexity of verification for parameterized systems under the assumptions of anonymity and asynchrony.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Negotiation Games (with abstract)

Negotiations, a model of concurrency with multi party negotiation as primitive, have been recently introduced in arXiv:1307.2145, arXiv:1403.4958. We initiate the study of games for this model. We study coalition problems: can a given coalition of agents force that a negotiation terminates (resp. block the negotiation so that it goes on forever)?; can the coalition force a given outcome of the negotiation? We show that for arbitrary negotiations the problems are EXPTIME-complete. Then we show that for sound and deterministic or even weakly deterministic negotiations the problems can be solved in PTIME. Notice that the input of the problems is a negotiation, which can be exponentially more compact than its state space.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification

This volume contains the proceedings of the Sixth International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2015). The symposium took place in Genoa, Italy, on the 21st and 22nd of September 2015. The proceedings of the symposium contain the abstracts of three invited talks and 13 papers that were accepted after a careful evaluation for presentation at the conference. The topics of the accepted papers cover algorithmic game theory, automata theory, formal verification, and modal and temporal logics.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

From LTL to Deterministic Automata: A Safraless Compositional Approach

We present a new algorithm to construct a deterministic Rabin automaton for an LTL formula $φ$. The automaton is the product of a master automaton and an array of slave automata, one for each $G$-subformula of $φ$. The slave automaton for $Gψ$ is in charge of recognizing whether $FGψ$ holds. As opposed to standard determinization procedures, the states of all our automata have a clear logical structure, which allows to apply various optimizations. Our construction subsumes former algorithms for fragments of LTL. Experimental results show improvement in the sizes of the resulting automata compared to existing methods.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Keeping a Crowd Safe: On the Complexity of Parameterized Verification (Corrected version)

We survey some results on the automatic verification of parameterized programs without identities. These are systems composed of arbitrarily many components, all of them running exactly the same finite-state program. We discuss the complexity of deciding that no component reaches an unsafe state. The note is addressed at theoretical computer scientists in general.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Computation of Summaries Using Net Unfoldings

We study the following summarization problem: given a parallel composition A=A1||...||An of labelled transition systems communicating with the environment through a distinguished component Ai, efficiently compute a summary Si such that E||A and E||Si are trace-equivalent for every environment E. While Si can be computed using elementary automata theory, the resulting algorithm suffers from the state-explosion problem. We present a new, simple but subtle algorithm based on net unfoldings, a partial-order semantics, give some experimental results using an implementation on top of MOLE, and show that our algorithm can handle divergences and compute weighted summaries with minor modifications.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

On Negotiation as Concurrency Primitive

We introduce negotiations, a model of concurrency close to Petri nets, with multiparty negotiation as primitive. We study the problems of soundness of negotiations and of, given a negotiation with possibly many steps, computing a summary, i.e., an equivalent one-step negotiation. We provide a complete set of reduction rules for sound, acyclic, weakly deterministic negotiations and show that, for deterministic negotiations, the rules compute the summary in polynomial time.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Parameterized Verification of Asynchronous Shared-Memory Systems

We characterize the complexity of the safety verification problem for parameterized systems consisting of a leader process and arbitrarily many anonymous and identical contributors. Processes communicate through a shared, bounded-value register. While each operation on the register is atomic, there is no synchronization primitive to execute a sequence of operations atomically. We analyze the complexity of the safety verification problem when processes are modeled by finite-state machines, pushdown machines, and Turing machines. The problem is coNP-complete when all processes are finite-state machines, and is PSPACE-complete when they are pushdown machines. The complexity remains coNP-complete when each Turing machine is allowed boundedly many interactions with the register. Our proofs use combinatorial characterizations of computations in the model, and in case of pushdown-systems, some language-theoretic constructions of independent interest.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

A Perfect Model for Bounded Verification

A class of languages C is perfect if it is closed under Boolean operations and the emptiness problem is decidable. Perfect language classes are the basis for the automata-theoretic approach to model checking: a system is correct if the language generated by the system is disjoint from the language of bad traces. Regular languages are perfect, but because the disjointness problem for CFLs is undecidable, no class containing the CFLs can be perfect. In practice, verification problems for language classes that are not perfect are often under-approximated by checking if the property holds for all behaviors of the system belonging to a fixed subset. A general way to specify a subset of behaviors is by using bounded languages (languages of the form w1* ... wk* for fixed words w1,...,wk). A class of languages C is perfect modulo bounded languages if it is closed under Boolean operations relative to every bounded language, and if the emptiness problem is decidable relative to every bounded language. We consider finding perfect classes of languages modulo bounded languages. We show that the class of languages accepted by multi-head pushdown automata are perfect modulo bounded languages, and characterize the complexities of decision problems. We also show that bounded languages form a maximal class for which perfection is obtained. We show that computations of several known models of systems, such as recursive multi-threaded programs, recursive counter machines, and communicating finite-state machines can be encoded as multi-head pushdown automata, giving uniform and optimal underapproximation algorithms modulo bounded languages.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Deterministic Automata for the (F,G)-fragment of LTL

When dealing with linear temporal logic properties in the setting of e.g. games or probabilistic systems, one often needs to express them as deterministic omega-automata. In order to translate LTL to deterministic omega-automata, the traditional approach first translates the formula to a non-deterministic Büchi automaton. Then a determinization procedure such as of Safra is performed yielding a deterministic ω-automaton. We present a direct translation of the (F,G)-fragment of LTL into deterministic ω-automata with no determinization procedure involved. Since our approach is tailored to LTL, we often avoid the typically unnecessarily large blowup caused by general determinization algorithms. We investigate the complexity of this translation and provide experimental results and compare them to the traditional method.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Proving Termination of Probabilistic Programs Using Patterns

Proving programs terminating is a fundamental computer science challenge. Recent research has produced powerful tools that can check a wide range of programs for termination. The analog for probabilistic programs, namely termination with probability one ("almost-sure termination"), is an equally important property for randomized algorithms and probabilistic protocols. We suggest a novel algorithm for proving almost-sure termination of probabilistic programs. Our algorithm exploits the power of state-of-the-art model checkers and termination provers for nonprobabilistic programs: it calls such tools within a refinement loop and thereby iteratively constructs a "terminating pattern", which is a set of terminating runs with probability one. We report on various case studies illustrating the effectiveness of our algorithm. As a further application, our algorithm can improve lower bounds on reachability probabilities.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Probabilistic Abstractions with Arbitrary Domains

Recent work by Hermanns et al. and Kattenbelt et al. has extended counterexample-guided abstraction refinement (CEGAR) to probabilistic programs. These approaches are limited to predicate abstraction. We present a novel technique, based on the abstract reachability tree recently introduced by Gulavani et al., that can use arbitrary abstract domains and widening operators (in the sense of abstract interpretation). We show how suitable widening operators can deduce loop invariants diffcult to find for predicate abstraction, and propose refinement techniques.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

Computing Least Fixed Points of Probabilistic Systems of Polynomials

We study systems of equations of the form X1 = f1(X1, ..., Xn), ..., Xn = fn(X1, ..., Xn), where each fi is a polynomial with nonnegative coefficients that add up to 1. The least nonnegative solution, say mu, of such equation systems is central to problems from various areas, like physics, biology, computational linguistics and probabilistic program verification. We give a simple and strongly polynomial algorithm to decide whether mu=(1, ..., 1) holds. Furthermore, we present an algorithm that computes reliable sequences of lower and upper bounds on mu, converging linearly to mu. Our algorithm has these features despite using inexact arithmetic for efficiency. We report on experiments that show the performance of our algorithms.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

Computing the Least Fixed Point of Positive Polynomial Systems

We consider equation systems of the form X_1 = f_1(X_1, ..., X_n), ..., X_n = f_n(X_1, ..., X_n) where f_1, ..., f_n are polynomials with positive real coefficients. In vector form we denote such an equation system by X = f(X) and call f a system of positive polynomials, short SPP. Equation systems of this kind appear naturally in the analysis of stochastic models like stochastic context-free grammars (with numerous applications to natural language processing and computational biology), probabilistic programs with procedures, web-surfing models with back buttons, and branching processes. The least nonnegative solution mu f of an SPP equation X = f(X) is of central interest for these models. Etessami and Yannakakis have suggested a particular version of Newton's method to approximate mu f. We extend a result of Etessami and Yannakakis and show that Newton's method starting at 0 always converges to mu f. We obtain lower bounds on the convergence speed of the method. For so-called strongly connected SPPs we prove the existence of a threshold k_f such that for every i >= 0 the (k_f+i)-th iteration of Newton's method has at least i valid bits of mu f. The proof yields an explicit bound for k_f depending only on syntactic parameters of f. We further show that for arbitrary SPP equations Newton's method still converges linearly: there are k_f>=0 and alpha_f>0 such that for every i>=0 the (k_f+alpha_f i)-th iteration of Newton's method has at least i valid bits of mu f. The proof yields an explicit bound for alpha_f; the bound is exponential in the number of equations, but we also show that it is essentially optimal. Constructing a bound for k_f is still an open problem. Finally, we also provide a geometric interpretation of Newton's method for SPPs.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

Space-efficient scheduling of stochastically generated tasks

We study the problem of scheduling tasks for execution by a processor when the tasks can stochastically generate new tasks. Tasks can be of different types, and each type has a fixed, known probability of generating other tasks. We present results on the random variable S^sigma modeling the maximal space needed by the processor to store the currently active tasks when acting under the scheduler sigma. We obtain tail bounds for the distribution of S^sigma for both offline and online schedulers, and investigate the expected value of S^sigma.

0 citations0 reviewsNo code linkedOpen access
preprint2009arXiv

Modeling and Verification for Timing Satisfaction of Fault-Tolerant Systems with Finiteness

The increasing use of model-based tools enables further use of formal verification techniques in the context of distributed real-time systems. To avoid state explosion, it is necessary to construct verification models that focus on the aspects under consideration. In this paper, we discuss how we construct a verification model for timing analysis in distributed real-time systems. We (1) give observations concerning restrictions of timed automata to model these systems, (2) formulate mathematical representations on how to perform model-to-model transformation to derive verification models from system models, and (3) propose some theoretical criteria how to reduce the model size. The latter is in particular important, as for the verification of complex systems, an efficient model reflecting the properties of the system under consideration is equally important to the verification algorithm itself. Finally, we present an extension of the model-based development tool FTOS, designed to develop fault-tolerant systems, to demonstrate %the benefits of our approach.

0 citations0 reviewsNo code linkedOpen access