III: Specification and Analysis of Multi-Actor Data-Driven Business Processes


NSF Award 1422375


PI: Victor Vianu, UCSD

Co-PI: Alin Deutsch, UCSD












Businesses and other organizations increasingly rely on electronic workflows

underlying business processes. These workflows are often centered around

a database and involve multiple interacting actors carrying out different roles.

They are typically very complex and prone to costly bugs, which leads

to the need for computer-aided design and analysis tools. These are critical

for increasing confidence in the robustness and correctness of complex

business processes.


The general objective of this project is to develop new techniques and tools for specifying,

analyzing, managing, and optimizing complex data-driven business processes,

with an explicit focus on the multi-actor setting.


This includes data sharing and updating, designing actor interface specifications to

the global workflow tailored to different roles, and specification of contractual obligations

among interacting actors. It will also consider runtime analysis tasks, including the

distributed monitoring of critical global properties, the use of local actor observations

to infer information about the global workflow, and validating autonomous offline

partial workflow executions by actors. The techniques and tools resulting

from this project will increase confidence in the robustness and correctness

of such systems, and enhance their functionality and efficiency. This will

benefit a wide variety of applications such as supply-chain management,

e-commerce, digital government and electronic health-care management.

The project will contribute to the development of human resources by training graduate

and undergraduate students in cutting-edge specification and static analysis

techniques which are crucial to business process management.


Achieving the objectives of the project requires fundamental advances in our understanding

of data-driven workflows involving multiple interacting actors. In the broader context of

software verification, the goals are particularly challenging because they involve the analysis

of infinite-state systems, whereas classical software verification typically deals with

finite-state abstractions. The project will extend the techniques recently developed for

data-driven workflows to the multi-actor scenario, and provide insight into the trade-off

between expressiveness of the specification language and tractability of analysis tasks.

The technical problems raised are intellectually challenging, and will bring into play

techniques from logic, automata theory, computational complexity, algorithms,

and computer-aided verification.






         Verification of Hierarchical Artifact Systems


Alin Deutsch, Yuliang Li, Victor Vianu

PODS 2016, to appear


         A Formal Study of Collaborative Access Control in Distributed Datalog


Serge Abiteboul, Pierre Bourhis, Victor Vianu

ICDT 2016

          Serge Abiteboul, Pierre Bourhis, Victor Vianu
          Theory of Computing Systems, 2015

Adrien Koutsos, Victor Vianu
         ICDT 2015

         Alin Deutsch, Richard Hull, Victor Vianu
         SIGMOD Record 43(3), 2014