1,721,092 research outputs found
Verification of choreographies during execution using the reactive event calculus
No full textThis article presents a run-time verification method of web service behaviour with respect to choreographies. We start from Dec- SerFlow as a graphical choreography description language. We select a core set of DecSerFlow elements and formalize them using a reactive version of the Event Calculus, based on the computational logic SCIFF framework. Our choice enables us to enrich DecSerFlow and the Event Calculus with quantitative time constraints and to model compensation actions
Solving Mathematical Puzzles: A Challenging Competition for AI
No full textRecently, a number of noteworthy results have been achieved in various fields of artificial intelligence, and many aspects of the problem-solving process have received significant attention by the scientific community. In this context, the extraction of comprehensive knowledge suitable for problem solving and reasoning, from textual and pictorial problem descriptions, has been less investigated, but recognized as essential for autonomous thinking in artificial intelligence. In this work we present a challenge where methods and tools for deep understanding are strongly needed for enabling problem solving: we propose to solve mathematical puzzles by means of computers, starting from text and diagrams describing them, without any human intervention. We are aware that the proposed challenge is hard and difficult to solve nowadays (and in the foreseeable future), but even studying and solving only single parts of the proposed challenge would represent an important step forward for artificial intelligence
Evaluating compliance: from LTL to abductive logic programming
No full textThe compliance verification task amounts to establishing if the execution of a system, given in terms of observed events, does re- spect a given property. In the past both the frameworks of Temporal Logics and Logic Programming have been extensively exploited to as- sess compliance. In this work we review the LTL and the Abductive Logic Programming frameworks in the light of compliance evaluation, and formally investigate the relationship between the two approaches. We define a notion of compliance within each approach, and then we show that an arbitrary LTL formula can be expressed in SCIFF, by pro- viding an automatic translation procedure from LTL to SCIFF which preserves compliance
Distributed Compliance Monitoring of Business Processes over MapReduce Architectures
No full textIn the era of IoT, large volumes of event data from different sources are collected in the form of streams. As these logs need to be online processed to extract further knowledge about the underlying business process, it is becoming more and more important to give support to run-time monitoring. In particular, increasing attention has been turned to conformance checking as a way to identify when a sequence of events deviates from the expected behavior. Albeit rather straightforward on a small log file, conformance verification techniques may show poor performance when dealing with big data, making increasingly attractive the possibility to improve scalability through distributed computation. In this paper, we adopt a previously implemented framework for compliance verification (which provides a high-level logic-based notation for the monitoring specification) and we show how it can be efficiently distributed on a set of computing nodes to support scalable run-time monitoring when dealing with large volumes of event logs
A distributed approach to compliance monitoring of business process event streams
Full text linkIn recent years, the significant advantages brought to business processes by process mining account for its evolution as a major concern in both industrial and academic research. In particular, increasing attention has been turned to compliance monitoring as a way to identify when a sequence of events deviates from the expected behaviour. As we are entering the IoT era, an increasing variety of smart objects can be introduced in business processes (e.g., tags to track products in a plant, smartphones and badge swiping to draw the activities of customers and employees in a shopping centre, etc.). All these objects produce large volumes of log data in the form of streams, which need to be run-time analysed to extract further knowledge about the underlying business process and to identify unexpected, non-conforming events. Albeit rather straightforward on a small log file, compliance verification techniques may show poor performances when dealing with big data and streams, thus calling for scalable approaches. This work investigates the possibility of spreading the compliance monitoring task over a network of computing nodes, achieving the desired scalability. The monitor is realised through the existing SCIFF framework for compliance checking, which provides a high level logic-based language for expressing the properties to be monitored and nicely supports the partitioning of the monitoring task. The distributed computation is achieved through a MapReduce approach and the adoption of an existing general engine for large scale stream processing. Experimental results show the feasibility of the approach as well as the advantages in performance brought to the compliance monitoring task
Map reduce autoscaling over the cloud with process mining monitoring
No full textOver the last years, the traditional pressing need for fast and reliable processing solutions has been further exacerbated by the increase of data volumes â produced by mobile devices, sensors and almost ubiquitous internet availability. These big data must be analyzed to extract further knowledge. Distributed programming models, such as Map Reduce, are providing a technical answer to this challenge. Furthermore, when relaying on cloud infrastructures, Map Reduce platforms can easily be runtime provided with additional computing nodes (e.g., the system administrator can scale the infrastructure to face temporal deadlines). Nevertheless, the execution of distributed programming models on the cloud still lacks automated mechanisms to guarantee the Quality of Service (i.e., autonomous scale-up/-down behavior). In this paper, we focus on the steps of monitoringMap Reduce applications (to detect situations where the temporal deadline will be exceeded) and performing recovery actions on the cluster (by automatically providing additional resources to boost the computation). To this end, we exploit some techniques and tools developed in the research field of Business Process Management: in particular, we focus on declarative languages and tools for monitoring the execution of business process. We introduce a distributed architecture where a logic-based monitor is able to detect possible delays, and trigger recovery actions such as the dynamic provisioning of a congruent number of resources
Abduction for Generating Synthetic Traces
No full textIn this paper we report our preliminary experience on the design of a generator of synthetic logs. Sometimes real logs might not be available, or their quality might not be good enough: synthetic logs instead can be generated with all the desired features and characteristics. Our tool takes as input a structured workflow model, encoded in the abductive declarative language SCIFF, and provides as output a log containing positive traces, i.e. traces deemed as conformant w.r.t. the model. Distinctive features of our approach are the capability of generating trace templates as well as grounded traces, the possibility of taking into account user-specified constraints on data and timestamps, and the capability of generating traces starting from a user-specified partial trace. Although our tool is still in its preliminary version, we have successfully exploited it to generate synthetic logs of different dimension, thus proving the viability of our approach
A Prolog application for reasoning on maths puzzles with diagrams
Full text linkDespite the indisputable progresses of artificial intelligence, some tasks that are rather easy for a human being are still challenging for a machine. An emblematic example is the resolution of mathematical puzzles with diagrams. Sub-symbolical approaches have proven successful in fields like image recognition and natural language processing, but the combination of these techniques into a multimodal approach towards the identification of the puzzle’s answer appears to be a matter of reasoning, more suitable for the application of a symbolic technique. In this work, we employ logic programming to perform spatial reasoning on the puzzle’s diagram and integrate the deriving knowledge into the solving process. Analysing the resolution strategies required by the puzzles of an international competition for humans, we draw the design principles of a Prolog reasoning library, which interacts with image processing software to formulate the puzzle’s constraints. The library integrates the knowledge from different sources, and relies on the Prolog inference engine to provide the answer. This work can be considered as a first step towards the ambitious goal of a machine autonomously solving a problem in a generic context starting from its textual-graphical presentation. An ability that can help potentially every human–machine interaction
Compliance in Business Processes with Incomplete Information and Time Constraints: a General Framework based on Abductive Reasoning
Full text linkThe capability to store data about Business Process (BP) executions in so-called Event Logs has brought to the identification of a range of key reasoning services (consistency, compliance, runtime monitoring, prediction) for the analysis of process executions and process models. Tools for the provision of these services typically focus on one form of reasoning alone. Moreover, they are often very rigid in dealing with forms of incomplete information about the process execution. While this enables the development of ad hoc solutions, it also poses an obstacle for the adoption of reasoning-based solutions in the BP community. In this paper, we introduce the notion of Structured Processes with Observability and Time (SPOT models), able to support incompleteness (of traces and logs), and temporal constraints on the activity duration and between activities. Then, we exploit the power of abduction to provide a flexible, yet computationally effective framework able to reinterpret key reasoning services in terms of incompleteness and observability in a uniform way
- …
