Narrow Results

Formalizing commonsense knowledge for reasoning about time has long been a central issue in AI. It has been recognized that the existing formalisms do not provide satisfactory solutions to some fundamental problems, viz. the frame problem. Moreover, it has turned out that the inferences drawn do not always coincide with those one had intended when one wrote the axioms. These issues call for a well-defined formalism and useful computational utilities for reasoning about time and change. Yoav Shoham of Stanford University introduced in his 1986 Yale doctoral thesis an appealing temporal nonmonotonic logic and identified a class of theories, causal theories, which have computationally simple model-theoretic properties. This paper is a study towards building upon Shoham's work on causal theories. We concentrate on improving computational aspects of causal theories while preserving their model-theoretic properties.

Online monitoring is essential to enhance the reliability for various systems including cyber-physical systems and Web services. During online monitoring, the system traces are checked against monitoring rules in real time to detect deviations from normal behaviors. In general, the rules are defined as boundary conditions by the experts of the monitored system. This work studies the problem of synthesizing online monitoring rules in the form of temporal logic formulas in an automated way. The monitoring rules are described as past-time signal temporal logic (ptSTL) formulas and an algorithm to synthesize such formulas from a given set of labeled system traces is proposed. The algorithm searches the formula space using genetic algorithms and produces the best formula representing a monitoring rule. In addition, online STL monitoring algorithm is improved to efficiently compute a quantitative valuation for piecewise-constant signals from ptSTL formulas, thus, to reduce the overhead of the real-time computation. The effectiveness of the results is shown on two illustrative examples inspired from online monitoring of Web services.

Formal verification of properties in reactive real-time systems is crucial, as these systems are often safety-critical. Such systems are successfully implemented using synchronous languages, where refinement is a relevant operation. This paper investigates the interplay between this operation and formal verification. It turns out that, while for the refined program component-based verification of properties expressed using suitable temporal logics is easily achieved, component-based verification from the point of view of the refining program is best achieved with observers. Our results are based on a translation of synchronous programs into Boolean automata. Their practical relevance is illustrated with a protocol case study.

Web engines crawl hyperlinks to search for new documents; yet when they index discovered documents they basically revert to conventional information retrieval models and concentrate on the indexing of terms in a single document.

We propose to overcome such limits with an approach based on temporal logic. By modeling a web site as a finite state transition system we are able to define complex and selective queries over hyperlinks with the aid of Computation Tree Logic operators.

We deployed the proposed approach in a prototype system that allows users pose queries in natural language. Queries are automatically translated in Computation Tree Logic, and the answer returned by our system is a set of paths. Experiments carried out with the aid of human experts show improved retrieval effectiveness with respect to current search engines.