Author name cluster

Alexei Lisitsa 0001

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

8 papers

1 author row

LOPSTR Conference 2021 Conference Paper

Representation and Processing of Instantaneous and Durative Temporal Phenomena

Manolis Pitsikalis
Alexei Lisitsa 0001
Shan Luo 0001

Abstract Event definitions in Complex Event Processing systems are constrained by the expressiveness of each system’s language. Some systems allow the definition of instantaneous complex events, while others allow the definition of durative complex events. While there are exceptions that offer both options, they often lack of intervals relations such as those specified by the Allen’s interval algebra. In this paper, we propose a new logic based temporal phenomena definition language, specifically tailored for Complex Event Processing. Our proposed language allows the representation of both instantaneous and durative phenomena and the temporal relations between them. Moreover, we demonstrate the expressiveness of our proposed language by employing a maritime use case where we define maritime events of interest. We analyse the execution semantics of our proposed language for stream processing and finally, we introduce and evaluate on real world data, Phenesthe, our open-source Complex Event Processing system.

Details

SAT Conference 2014 Conference Paper

A SAT Attack on the Erdős Discrepancy Conjecture

Boris Konev
Alexei Lisitsa 0001

Abstract In 1930s Paul Erdős conjectured that for any positive integer C in any infinite ±1 sequence ( x n ) there exists a subsequence x d, x 2 d, x 3 d, …, x kd, for some positive integers k and d, such that \(\mid \sum_{i=1}^k x_{id} \mid >C\). The conjecture has been referred to as one of the major open problems in combinatorial number theory and discrepancy theory. For the particular case of C = 1 a human proof of the conjecture exists; for C = 2 a bespoke computer program had generated sequences of length 1124 of discrepancy 2, but the status of the conjecture remained open even for such a small bound. We show that by encoding the problem into Boolean satisfiability and applying the state of the art SAT solver, one can obtain a discrepancy 2 sequence of length 1160 and a proof of the Erdős discrepancy conjecture for C = 2, claiming that no discrepancy 2 sequence of length 1161, or more, exists. We also present our partial results for the case of C = 3.

Details

TIME Conference 2011 Conference Paper

Temporal Access to the Iteration Sequences: A Unifying Approach to Fixed Point Logics

Alexei Lisitsa 0001

The semantics of fixed point constructions is commonly defined in terms of iteration sequences. For example, the least fixed point of a monotone operator consists of all points which eventually appear in the approximations computed iteratively. We take this temporal reading as the starting point and develop a systematic approach to temporal definitions over iteration sequences. As a result, we propose an extension of first-order predicate logic with an iterative operator, in which iteration steps may be accessed by temporal logic formulae. We show that proposed logic FO+TAI subsumes virtually all known deterministic fixed point extentions of first-order logic as its natural fragments. On the other hand we show that over finite structures FO+TAI has the same expressive power as FO+PFP (FO with partial fixed point operator), but in many cases providing with more concise definitions. Finally, we show that the extension of modal mu-calculus with the temporal access leads to the more expressive logic closed under assume-guarantee specifications operator.

Details

TIME Conference 2008 Conference Paper

Practical First-Order Temporal Reasoning

Clare Dixon
Michael Fisher 0001
Boris Konev
Alexei Lisitsa 0001

In this paper we consider the specification and verification of infinite-state systems using temporal logic. In particular, we describe parameterised systems using a new variety of first-order temporal logic that is both powerful enough for this form of specification and tractable enough for practical deductive verification. Importantly, the power of the temporal language allows us to describe (and verify) asynchronous systems, communication delays and more complex liveness and fairness properties. These aspects appear difficult for many other approaches to infinite-state verification.

Details

TIME Conference 2006 Conference Paper

In time alone: on the computational power of querying the history

Alexei Lisitsa 0001
Igor Potapov

Querying its own history is an important mechanism in the computations, especially those interacting with people or other computations such as transaction processing, electronic data interchange. In this paper we study the computational power of referring to the past primitive. To do that we propose a refined formal model, history dependent machine (RDM), which uses querying the history as its sole computational primitive. Our main result may be spelled in general terms as: a model with a single agent wandering around a pool of resources and having ability to check its own history for simple temporal properties has a universal computational power. Moreover, RDM can simulate any multicounter machine in real time. Then we show that the computations of RDM may be specified in the extension of propositional linear temporal logic by flexible constants, the abstraction operator and equality. We use then universality of RDM model to show that the above extension with a single flexible constant is not recursively axiomatizable

Details

TIME Conference 2005 Conference Paper

Temporal Logic with Predicate lambda-Abstraction

Alexei Lisitsa 0001
Igor Potapov

A predicate linear temporal logic LTL/sub /spl lambda/=/ without quantifiers but with predicate /spl lambda/-abstraction mechanism and equality is considered. The models of LTL/sub /spl lambda/=/ can be naturally seen as the systems of pebbles (flexible constants) moving over the elements of some (possibly infinite) domain. This allows to use LTL/sub /spl lambda/=/ for the specification of dynamic systems using some resources, such as processes using memory locations, mobile agents occupying some sites, etc. On the other hand we show that LTL/sub /spl lambda/=/ is not recursively axiomatizable and, therefore, fully automated verification of LTL/sub /spl lambda/=/ specifications via validity checking is not, in general, possible. The result is based on computational universality of the above abstract computational model of pebble systems, which is of independent interest due to the range of possible interpretations of such systems.

Details

MFCS Conference 2004 Conference Paper

Membership and Reachability Problems for Row-Monomial Transformations

Alexei Lisitsa 0001
Igor Potapov

Abstract In this paper we study the membership and vector reachability problems for labelled transition systems with row-monomial transformations. We show the decidability of these problems for row-monomial martix semigroups over rationals and extend these results to the wider class of matrix semigroups. After that we apply our methods to reachability problems for a class of transition systems which turn out to be equivalent to specific counter machines.

Details

LPAR Conference 2002 Conference Paper

Searching for Invariants Using Temporal Resolution

James Brotherston
Anatoli Degtyarev
Michael Fisher 0001
Alexei Lisitsa 0001

Abstract In this paper, we show how the clausal temporal resolution technique developed for temporal logic provides an effective method for searching for invariants, and so is suitable for mechanising a wide class of temporal problems. We demonstrate that this scheme of searching for invariants can be also applied to a class of multi-predicate induction problems represented by mutually recursive definitions. Completeness of the approach, examples of the application of the scheme, and overview of the implementation are described.

Details