Publication

Symbolic Proof of CTL Formulae over Petri Nets

Publications associées (33)

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Connectez-vous pour utiliser Chat avec Graph Search

The Kaldi Speech Recognition Toolkit

Petr Motlicek

We describe the design of Kaldi, a free, open-source toolkit for speech recognition research. Kaldi provides a speech recognition system based on finite-state automata (using the freely available OpenFst), together with detailed documentation and a compreh ...

Idiap2012

Verification of consensus algorithms using satisfiability solving

André Schiper

Consensus is at the heart of fault-tolerant distributed computing systems. Much research has been devoted to developing algorithms for this particular problem. This paper presents a semi-automatic verification approach for asynchronous consensus algorithms ...

Springer Verlag2011

Model checking transactional memories

Rachid Guerraoui, Vasu Singh

Model checking transactional memories (TMs) is difficult because of the unbounded number, length, and delay of concurrent transactions, as well as the unbounded size of the memory. We show that, under certain conditions satisfied by most TMs we know of, th ...

Springer Verlag2010

Model checking: Algorithmic verification and debugging

Joseph Sifakis

Turing Lecture from the winners of the 2007 ACM A.M. Turing Award.In 1981, Edmund M. Clarke and E. Allen Emerson, working in the USA, and Joseph Sifakis working independently in France, authored seminal papers that founded what has become the highly succes ...

2009

Asymmetric information embedding

Mohammad Amin Shokrollahi

In the Information Embedding Problem one is given a piece of data which can be altered only conditionally, for example only at certain places. One is then asked to embed an arbitrary message into the data by only applying admissible changes to the data. Th ...

Springer-Verlag2008

From Liveness to Promptness

Liveness temporal properties state that something

good'' eventually happens, e.g., every request is eventually granted. In Linear Temporal Logic (LTL), there is no a priori bound on the

wait time'' for an eventually to be fulfilled. That is,

F\theta

...

2007

Soundness and Equivalence of Petri Nets and Annotated Finite State Automate: A Comparison in the SOA Context

A lot of work exists on notions of equivalence and soundness relations of different workflow models, which are used in different domains like e.g. Business Process Modeling, Software and Service Engineering. These definitions are based on different models, ...

IEEE2007

Algorithms for Interface Synthesis

Vasu Singh, Dirk Thilo Beyer

A temporal interface for a software component is a ﬁnite automaton that speciﬁes the legal sequences of calls to functions that are provided by the component. We compare and evaluate three different algorithms for automatically extracting temporal interfac ...

Springer2007

Supporting Loop Proofs in KeY by using BLAST

Mathias Krebs

In contrast to beta-testing, formal verification can guarantee correctness of a program against a specification. Two basic verification techniques are theorem proving and model checking. Both have strengths and weaknesses. Theorem proving is powerful, but ...

2006

When Birds Die: Making Population Protocols Fault-tolerant

Rachid Guerraoui, Eric Ruppert

In the population protocol model introduced by Angluin et al. [2], a collection of agents, which are modelled by finite state machines, move around unpredictably and have pairwise interactions. The ability of such systems to compute functions on a multiset ...

2006

From Liveness to Promptness

Liveness temporal properties state that something

good'' eventually happens, e.g., every request is eventually granted. In Linear Temporal Logic (LTL), there is no a priori bound on the

wait time'' for an eventually to be fulfilled. That is,

F\theta

...

2007