Source author record

Ario Santoso

Ario Santoso appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Catalog footprint

What is connected

5works
2topics
4close collaborators

Actions

Connect this record

Log in to claim

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

5 published item(s)

preprint2016arXiv

Verification of Data-aware Business Processes in the Presence of Ontologies

The meet up between data, processes and structural knowledge in modeling enterprise systems is a challenging task that has led to the study of combining formalisms from knowledge representation, database theory, and process management. To ensure system correctness, formal verification also comes into play and offers well-established techniques. In line with this, significant results have been obtained within the research on data-aware business processes (DABP), which studies the marriage between static and dynamic aspects of a system within a unified framework. Here, we investigate the verification of DABP in the presence of ontologies, and provide the following contributions: (1) We propose a formal framework called Golog-KABs (GKABs), by leveraging on the state of the art formalisms for DABP equipped with ontologies. GKABs enable us to specify semantically-rich DABP, where the system dynamics are specified using a high-level action language inspired by the Golog programming language. (2) We propose a parametric execution semantics for GKABs that is able to elegantly accommodate a plethora of inconsistency-aware semantics based on the well-known notion of repair, and this leads us to several variants of inconsistency-aware GKABs. (3) We enhance GKABs towards context-sensitive GKABs. (4) We introduce the so-called Alternating-GKABs that allow for a more fine-grained analysis over the systems. (5) We introduce a novel framework called Semantically-Enhanced Data-Aware Processes (SEDAPs) that, by utilizing ontologies, enable us to have a high-level conceptual view over the evolution of the underlying system. We also provide reductions for the verification of sophisticated first-order temporal properties over all of the settings above, and show that verification can be addressed using existing techniques developed for Data-Centric Dynamic Systems (a well-established DABP framework).

preprint2015arXiv

Verification of Generalized Inconsistency-Aware Knowledge and Action Bases (Extended Version)

Knowledge and Action Bases (KABs) have been put forward as a semantically rich representation of a domain, using a DL KB to account for its static aspects, and actions to evolve its extensional part over time, possibly introducing new objects. Recently, KABs have been extended to manage inconsistency, with ad-hoc verification techniques geared towards specific semantics. This work provides a twofold contribution along this line of research. On the one hand, we enrich KABs with a high-level, compact action language inspired by Golog, obtaining so called Golog-KABs (GKABs). On the other hand, we introduce a parametric execution semantics for GKABs, so as to elegantly accomodate a plethora of inconsistency-aware semantics based on the notion of repair. We then provide several reductions for the verification of sophisticated first-order temporal properties over inconsistency-aware GKABs, and show that it can be addressed using known techniques, developed for standard KABs.

preprint2014arXiv

Adding Context to Knowledge and Action Bases

Knowledge and Action Bases (KABs) have been recently proposed as a formal framework to capture the dynamics of systems which manipulate Description Logic (DL) Knowledge Bases (KBs) through action execution. In this work, we enrich the KAB setting with contextual information, making use of different context dimensions. On the one hand, context is determined by the environment using context-changing actions that make use of the current state of the KB and the current context. On the other hand, it affects the set of TBox assertions that are relevant at each time point, and that have to be considered when processing queries posed over the KAB. Here we extend to our enriched setting the results on verification of rich temporal properties expressed in mu-calculus, which had been established for standard KABs. Specifically, we show that under a run-boundedness condition, verification stays decidable.

preprint2013arXiv

Verification of Inconsistency-Aware Knowledge and Action Bases (Extended Version)

Description Logic Knowledge and Action Bases (KABs) have been recently introduced as a mechanism that provides a semantically rich representation of the information on the domain of interest in terms of a DL KB and a set of actions to change such information over time, possibly introducing new objects. In this setting, decidability of verification of sophisticated temporal properties over KABs, expressed in a variant of first-order mu-calculus, has been shown. However, the established framework treats inconsistency in a simplistic way, by rejecting inconsistent states produced through action execution. We address this problem by showing how inconsistency handling based on the notion of repairs can be integrated into KABs, resorting to inconsistency-tolerant semantics. In this setting, we establish decidability and complexity of verification.

preprint2013arXiv

Verification of Semantically-Enhanced Artifact Systems (Extended Version)

Artifact-Centric systems have emerged in the last years as a suitable framework to model business-relevant entities, by combining their static and dynamic aspects. In particular, the Guard-Stage-Milestone (GSM) approach has been recently proposed to model artifacts and their lifecycle in a declarative way. In this paper, we enhance GSM with a Semantic Layer, constituted by a full-fledged OWL 2 QL ontology linked to the artifact information models through mapping specifications. The ontology provides a conceptual view of the domain under study, and allows one to understand the evolution of the artifact system at a higher level of abstraction. In this setting, we present a technique to specify temporal properties expressed over the Semantic Layer, and verify them according to the evolution in the underlying GSM model. This technique has been implemented in a tool that exploits state-of-the-art ontology-based data access technologies to manipulate the temporal properties according to the ontology and the mappings, and that relies on the GSMC model checker for verification.