Author name cluster

Alin Deutsch

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.

4 papers

1 author row

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.

Details

KR Conference 2014 Conference Paper

State-Boundedness in Data-Aware Dynamic Systems

Babak Bagheri Hariri
Diego Calvanese
Marco Montali
Alin Deutsch

verification turns out to be undecidable even for propositional reachability properties (Deutsch et al. 2009; Belardinelli, Lomuscio, and Patrizi 2012; Bagheri Hariri et al. 2013b; 2013a). To mitigate this problem, an extensive amount of research has been devoted to find suitable classes of data-aware dynamic systems for which verification of first-order temporal properties becomes decidable. In particular, a plethora of recent works has shown that verification of data-aware dynamic systems working over unboundedly many data is decidable even for very rich temporal logics, provided that the system is state-bounded. For example, Belardinelli, Lomuscio, and Patrizi (2012) show decidability of verification of state-bounded (there called b-bounded) artifact centric multiagent systems (ACMASs) for a first-order, epistemic variant of CTL, with active domain quantification that applies across time points. Bagheri Hariri et al. (2013b) give a key decidability result for the verification of state-bounded Data-Centric Dynamic Systems (DCDSs) against a first-order variant of the µ-calculus with a limited form of quantification across time. Within the research line of reasoning about actions, De Giacomo, Lesperance, and Patrizi (2012) show that (state-)bounded Situation Calculus theories can be verified against a first-order variant of the µ-calculus, without quantification across states. Notably, in all these cases stateboundedness guarantees the existence of a faithful (sound and complete) finite-state abstraction of the system, paving the way for the application of standard model checking tools. Verification of dynamic systems that manipulate data, stored in a database or ontology, has lately received increasing attention. A plethora of recent works has shown that verification of systems working over unboundedly many data is decidable even for very rich temporal properties, provided that the system is state-bounded. This condition requires the existence of an overall bound on the amount of data stored in each single state along the system evolution. In general, checking stateboundedness is undecidable. An open question is whether it is possible to isolate significant classes of dynamic systems for which state-boundedness is decidable. In this paper we provide a strong negative answer, by resorting to a novel connection with variants of Petri nets. In particular, we show undecidability for systems whose data component contains unary relations only, and whose action component queries and updates such relations in a very limited way. To contrast this result, we propose interesting relaxations of the sufficient conditions proposed in the concrete setting of Data-Centric Dynamic Systems, building on recent results on chase termination for tuple-generating dependencies.

TCS Journal 2007 Journal Article

Rewriting queries using views with access patterns under integrity constraints

Alin Deutsch
Bertram Ludäscher
Alan Nash

We study the problem of rewriting queries using views in the presence of access patterns, integrity constraints, disjunction and negation. We provide asymptotically optimal algorithms for (1) finding minimally containing and (2) maximally contained rewritings respecting the access patterns (which we call executable) and for (3) deciding whether an exact executable rewriting exists. We show that rewriting queries using views in this case reduces (a) to rewriting queries with access patterns and constraints without views and also (b) to rewriting queries using views under constraints without access patterns. We show how to solve (a) directly and how to reduce (b) to rewriting queries under constraints only (semantic optimization). These reductions provide two separate routes to a unified solution for problems 1, 2 and 3 based on an extension of the relational chase theory to queries and constraints with disjunction and negation. We also handle equality and arithmetic comparisons. We also show that in an information integration setting, maximally contained rewritings are given by the certain answers (under the usual semantics) for a set of constraints derived from the binding patterns. That is, except for defining the appropriate constraints, binding patterns do not need special treatment. Finally, we show that if there is an exact executable rewriting, there is an executable rewriting which is a union of conjunctive queries with negation.

Details DOI

TCS Journal 2005 Journal Article

XML queries and constraints, containment and reformulation

Alin Deutsch
Val Tannen

Starting from the XQuery language we define XBind, an XML analog of relational conjunctive queries as well as a related class of XML integrity constraints (dependencies). We identify a fragment of XBind for which containment is decidable, in fact Π 2 p -complete, and a further fragment for which containment is NP-complete. We extend the containment algorithm to take XML dependencies into account. We give an algorithm for the reformulation of XBind queries under combinations of GAV and LAV XQuery views, as well as additional dependencies. We prove a completeness theorem which guarantees that under certain conditions, our algorithm will find a minimal reformulation if one exists. Moreover, we identify conditions when this algorithm achieves optimal complexity bounds. Our results on containment and reformulation depend on certain restrictions on the query and constraint languages. We calibrate the results by showing that lifting these restrictions significantly changes the complexity of the problems.

Details DOI