Victor Vianu

Highlights Conference 2016 Conference Abstract

Verification of Hierarchical Artifact Systems

• Alin Deutsch
• Yuliang Li
• Victor Vianu

The proposed talk will present results from a PODS 2016 paper with the same title, co-authored with Alin Deutsch and Yuliang Li (UC San Diego). The past decade has witnessed the evolution of workflow specification frameworks from the traditional process-centric approach towards data-awareness. Process-centric formalisms focus on control flow while under-specifying the underlying data and its manipulations by the process tasks, often abstracting them away completely. In contrast, data-aware formalisms treat data as first-class citizens. A notable exponent of this class is IBM’s business artifact model which has been successfully deployed in practice and adopted in industrial standards. In a nutshell, artifacts consist of data that is updated by a set of services that implement business process tasks, specified declaratively by pre-and-post conditions. IBM has developed several variants of artifacts, of which the most recent is Guard-Stage-Milestone (GSM). The GSM approach provides rich structuring mechanisms for services, including parallelism, concurrency and hierarchy, and has been incorporated in the OMG standard for Case Management Model and Notation (CMMN). The artifact approach has spawned a rich body of research in academia, focused primarily on verification. The present work represents a significant advance on the artifact verification problem on several fronts. We consider a much richer and more realistic model, called Hierarchical Artifact System (HAS), abstracting core elements of the GSM model. In particular, the model features task hierarchy, concurrency, and richer artifact data (including updatable artifact relations). We consider properties expressed in a novel hierarchical temporal logic, HLTL-FO, that is well-suited to the model. Our main results establish the complexity of checking HLTL-FO properties for various classes of HAS, highlighting the impact of various features on verification. The results require qualitatively new techniques, because the reduction to finite-state model checking used in previous work is no longer possible. Instead, the richer model requires the use of a hierarchy of Vector Addition Systems with States (VASS). The arithmetic constraints are handled using quantifier elimination techniques, adapted to our setting. The talk will present some of the mathematical intuition behind the results, focusing on two of my favorite aspects: (i) the use of Vector Addition Systems to handle unbounded evolving data, and (ii) the new hierarchical variant of LTL-FO.

TCS Journal 2003 Journal Article

Foreword

• Jan Van den Bussche
• Victor Vianu

MFCS Conference 2001 Conference Paper

Towards Regular Languages over Infinite Alphabets

• Frank Neven
• Thomas Schwentick
• Victor Vianu

Abstract Motivated by formal models recently proposed in the context of XML, we study automata and logics on strings over infinite alphabets. These are conservative extensions of classical automata and logics defining the regular languages on finite alphabets. Specifically, we consider register and pebble automata, and extensions of first-order logic and monadic second-order logic. For each type of automaton we consider oneway and two-way variants, as well as deterministic, non-deterministic, and alternating control. We investigate the expressiveness and complexity of the automata, their connection to the logics, as well as standard decision problems.

TCS Journal 2000 Journal Article

Queries and computation on the web

• Serge Abiteboul
• Victor Vianu

The paper introduces a model of the Web as an infinite, semistructured set of objects. We reconsider the classical notions of genericity and computability of queries in this new context and relate them to styles of computation prevalent on the Web, based on browsing and searching. We revisit several well-known declarative query languages (first-order logic, Datalog, and Datalog with negation) and consider their computational characteristics in terms of the notions introduced in this paper. In particular, we are interested in languages or fragments thereof which can be implemented by browsing, or by browsing and searching combined. Surprisingly, stratified and well-founded semantics for negation turn out to have basic shortcomings in this context, while inflationary semantics emerges as an appealing alternative.

CSL Conference 1999 Invited Paper

Topological Queries in Spatial Databases

• Victor Vianu

Abstract Handling spatial information is required by many database applications, and each poses different requirements on query languages. In many cases the precise size of the regions is important, while in other applications we may only be interested in the TOPOLOGICAL relations- hips between regions — intuitively, those that pertain to adjacency and connectivity properties of the regions, and are therefore invariant under homeomorphisms. Such differences in scope and emphasis are crucial, as they affect the data model, the query language, and performance. This talk focuses on queries targeted towards topological information for two- dimensional spatial databases, where regions are specified by polynomial inequalities with integer coeficients. We focus on two main aspects: (i) languages for expressing topological queries, and (ii) the representation of topological information. In regard to (i), we study several languages geared towards topological queries, building upon well-known topologi- cal relationships between pairs of planar regions proposed by Egenhofer. In regard to (ii), we show that the topological information in a spatial database can be precisely summarized by a finite relational database which can be viewed as a topological annotation to the raw spatial data. All topological queries can be answered using this annotation, called to- pological invariant. This yields a potentially more economical evaluation strategy for such queries, since the topological invariant is generally much smaller than the raw data. We examine in detail the problem of transla- ting topological queries against the spatial database into queries against the topological invariant. The languages considered are first-order on the spatial database side, and fixpoint and first-order on the topological in- variant side. In particular, it is shown that fixpoint expresses precisely the PTIME queries on topological invariants. This suggests that topolo- gical invariants are particularly well-behaved with respect to descriptive complexity. (Based on joint work with C. H. Papadimitriou, D. Suciu and L. Segoufin.)

TCS Journal 1998 Journal Article

A probabilistic view of Datalog parallelization

• Sérgio Lifschitz
• Victor Vianu

We explore an approach to developing Datalog parallelization strategies that aims at good expected rather than worst-case performance. To illustrate, we consider a very simple parallelization strategy that applies to all Datalog programs. We prove that this has very good expected performance under equal distribution of inputs. This is done using an extension of 0–1 laws adapted to this context. The analysis is confirmed by experimental results on randomly generated data.

TCS Journal 1995 Journal Article

Computing with infinitary logic

• Serge Abiteboul
• Moshe Y. Vardi
• Victor Vianu

Most recursive extensions of the first-order queries converge around two central classes of queries: fixpoint and while. Infinitary logic (with finitely many variables) is a very powerful extension of these languages which provides an elegant unifying formalism for a wide variety of query languages. However, neither the syntax nor the semantics of infinitary logic are effective, and its connection to practical query languages has been largely unexplored. We relate infinitary logic to another powerful extension of fixpoint and while, called relational machine, which highlights the computational style of these languages. Relational machines capture the kind of computation occurring when a query language is embedded in a host programming language, as in C+SQL. The main result of this paper is that relational machines correspond to the natural effective fragment of infinitary logic. Other well-known query languages are related to infinitary logic using syntactic restrictions formulated in language-theoretic terms. For example, it is shown that while corresponds to infinitary logic formulas which can be described by a regular language. As a side effect to these results, we obtain interesting normal forms for effective infinitary logic formulas.

TCS Journal 1992 Journal Article

Conceptual level concurrency control of relational update transactions

• Victor Vianu
• Gottfried Vossen

The concurrency control problem is examined for transactions as they appear at the conceptual level in a concrete database model. Specifically, a class of widely accepted update transactions in relational databases is studied with respect to concurrency control. It is shown how static serializability testing, as well as dynamic scheduling, can be improved by making use of the semantic information available at the conceptual level on transactions and database constraints.

STOC Conference 1991 Conference Paper

Generic Computation and Its Complexity

• Serge Abiteboul
• Victor Vianu

TCS Journal 1990 Journal Article

Parallel update transactions

• Dino Karabeg
• Victor Vianu

MFCS Conference 1977 Conference Paper

The Bodnarchuk Metric Space of Languages and the Topology of the Learning Space

• Victor Vianu