Concept

Logique temporelle linéaire

Publications associées (62)

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

A Sparsity Constraint for Topic Models - Application to Temporal Activity Mining

Jean-Marc Odobez, Rémi Emonet, Jagannadan Varadarajan

We address the mining of sequential activity patterns from document logs given as word-time occurrences. We achieve this using topics that models both the cooccurrence and the temporal order in which words occur within a temporal window. Discovering such t ...

2010

A Sparsity Constraint for Topic Models - Application to Temporal Activity Mining

Jean-Marc Odobez, Rémi Emonet, Jagannadan Varadarajan

Idiap2010

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

Human Gait Analysis and Classification Based on Neural Networks and Fuzzy Logic

Rafal Tomasz Dlugosz

Human gait analysis and classification is the process of identifying individuals by their walking manners. Computerized gait analysis using neural networks and fuzzy logic has become an integral part of the treatment decision-making process. Authors propos ...

2009

On Joint Modelling of Grapheme and Phoneme Information using KL-HMM for ASR

Hervé Bourlard, Guillermo Aradilla

In this paper, we propose a simple approach to jointly model both grapheme and phoneme information using Kullback-Leibler divergence based HMM (KL-HMM) system. More specifically, graphemes are used as subword units and phoneme posterior probabilities estim ...

Idiap2009

Completeness and Nondeterminism in Model Checking Transactional Memories

Rachid Guerraoui, Vasu Singh

Software transactional memory (STM) offers a disciplined concurrent programming model for exploiting the parallelism of modern processor architectures. This paper presents the first \emph{deterministic} specification automata for strict serializability and ...

Springer2008

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

Evolving Objects in Temporal Information Systems

Stefano Spaccapietra, Christine Parent

This paper presents a semantic foundation of temporal conceptual models used to design temporal information systems. We consider a modelling language able to express both timestamping and evolution constraints. We conduct a deeper investigation of evolutio ...

2007

Detecting Malicious Code by Model Checking

Johannes Kinder

The ease of compiling malicious code from source code in higher programming languages has increased the volatility of malicious programs: The first appearance of a new worm in the wild is usually followed by modified versions in quick succession. As demons ...

Springer2005

Coordinating Agile Vehicles through the Model-based Execution of Temporal Plans

Thomas Léauté

Agile autonomous systems are emerging, such as unmanned aerial vehicles (UAVs), that must robustly perform tightly coordinated time-critical missions; for example, military surveillance or search-and-rescue scenarios. In the space domain, execution of temp ...

AAAI Press / The MIT Press2005

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