Monitoring Complex Processes to Verify System Conformance: A Declarative Rule-Based Framework

Over the last 60 years, computers and software have favoured incredible advancements in every field. Nowadays, however, these systems are so complicated that it is difficult – if not challenging – to understand whether they meet some requirement or are able to show some desired behaviour or property. This dissertation introduces a Just-In-Time (JIT) a posteriori approach to perform the conformance check to identify any deviation from the desired behaviour as soon as possible, and possibly apply some corrections. The declarative framework that implements our approach – entirely developed on the promising open source forward-chaining Production Rule System (PRS) named Drools – consists of three components: 1. a monitoring module based on a novel, efficient implementation of Event Calculus (EC), 2. a general purpose hybrid reasoning module (the first of its genre) merging temporal, semantic, fuzzy and rule-based reasoning, 3. a logic formalism based on the concept of expectations introducing Event-Condition-Expectation rules (ECE-rules) to assess the global conformance of a system. The framework is also accompanied by an optional module that provides Probabilistic Inductive Logic Programming (PILP). By shifting the conformance check from after execution to just in time, this approach combines the advantages of many a posteriori and a priori methods proposed in literature. Quite remarkably, if the corrective actions are explicitly given, the reactive nature of this methodology allows to reconcile any deviations from the desired behaviour as soon as it is detected. In conclusion, the proposed methodology brings some advancements to solve the problem of the conformance checking, helping to fill the gap between humans and the increasingly complex technology.

Certificates for Incremental Type Checking

The central topic of this thesis is the study of algorithms for type checking, both from the programming language and from the proof-theoretic point of view. A type checking algorithm takes a program or a proof, represented as a syntactical object, and checks its validity with respect to a specification or a statement. It is a central piece of compilers and proof assistants. We postulate that since type checkers are at the interface between proof theory and program theory, their study can let these two fields mutually enrich each other. We argue by two main instances: first, starting from the problem of proof reuse, we develop an incremental type checker; secondly, starting from a type checking program, we evidence a novel correspondence between natural deduction and the sequent calculus.

Non-normal modal logics, quantification, and deontic dilemmas. A study in multi-relational semantics

This dissertation is devoted to the study of non-normal (modal) systems for deontic logics, both on the propositional level, and on the first order one. In particular we developed our study the Multi-relational setting that generalises standard Kripke Semantics. We present new completeness results concerning the semantic setting of several systems which are able to handle normative dilemmas and conflicts. Although primarily driven by issues related to the legal and moral field, these results are also relevant for the more theoretical field of Modal Logic itself, as we propose a syntactical, and semantic study of intermediate systems between the classical propositional calculus CPC and the minimal normal modal logic K.

Type Systems for Distributed Programs: Components and Sessions

Modern software systems, in particular distributed ones, are everywhere around us and are at the basis of our everyday activities. Hence, guaranteeing their cor- rectness, consistency and safety is of paramount importance. Their complexity makes the verification of such properties a very challenging task. It is natural to expect that these systems are reliable and above all usable. i) In order to be reliable, compositional models of software systems need to account for consistent dynamic reconfiguration, i.e., changing at runtime the communication patterns of a program. ii) In order to be useful, compositional models of software systems need to account for interaction, which can be seen as communication patterns among components which collaborate together to achieve a common task. The aim of the Ph.D. was to develop powerful techniques based on formal methods for the verification of correctness, consistency and safety properties related to dynamic reconfiguration and communication in complex distributed systems. In particular, static analysis techniques based on types and type systems appeared to be an adequate methodology, considering their success in guaranteeing not only basic safety properties, but also more sophisticated ones like, deadlock or livelock freedom in a concurrent setting. The main contributions of this dissertation are twofold. i) On the components side: we design types and a type system for a concurrent object-oriented calculus to statically ensure consistency of dynamic reconfigurations related to modifications of communication patterns in a program during execution time. ii) On the communication side: we study advanced safety properties related to communication in complex distributed systems like deadlock-freedom, livelock- freedom and progress. Most importantly, we exploit an encoding of types and terms of a typical distributed language, session π-calculus, into the standard typed π- calculus, in order to understand their expressive power.

Proof theory of quantified modal logics

We introduce labelled sequent calculi for indexed modal logics. We prove that the structural rules of weakening and contraction are height-preserving admissible, that all rules are invertible, and that cut is admissible. Then we prove that each calculus introduced is sound and complete with respect to the appropriate class of transition frames.

Engineering Complex Computational Ecosystems

Self-organising pervasive ecosystems of devices are set to become a major vehicle for delivering infrastructure and end-user services. The inherent complexity of such systems poses new challenges to those who want to dominate it by applying the principles of engineering. The recent growth in number and distribution of devices with decent computational and communicational abilities, that suddenly accelerated with the massive diffusion of smartphones and tablets, is delivering a world with a much higher density of devices in space. Also, communication technologies seem to be focussing on short-range device-to-device (P2P) interactions, with technologies such as Bluetooth and Near-Field Communication gaining greater adoption. Locality and situatedness become key to providing the best possible experience to users, and the classic model of a centralised, enormously powerful server gathering and processing data becomes less and less efficient with device density. Accomplishing complex global tasks without a centralised controller responsible of aggregating data, however, is a challenging task. In particular, there is a local-to-global issue that makes the application of engineering principles challenging at least: designing device-local programs that, through interaction, guarantee a certain global service level. In this thesis, we first analyse the state of the art in coordination systems, then motivate the work by describing the main issues of pre-existing tools and practices and identifying the improvements that would benefit the design of such complex software ecosystems. The contribution can be divided in three main branches. First, we introduce a novel simulation toolchain for pervasive ecosystems, designed for allowing good expressiveness still retaining high performance. Second, we leverage existing coordination models and patterns in order to create new spatial structures. Third, we introduce a novel language, based on the existing ``Field Calculus'' and integrated with the aforementioned toolchain, designed to be usable for practical aggregate programming.

Prävalenz dentaler Pathologien vergangener und rezenter Bevölkerungen : dentalpathologische Untersuchungen an einem frühmittelalterlichen Reihengräberfeld aus Mannheim

Pathologische Veränderungen des stomatognathen Systems haben die Menschheit seit jeher geplagt. Etliche dieser dentalen Pathologien hinterlassen Spuren, die auch an Skelettmaterial noch erkannt werden können. Die vorliegende Studie beschäftigt sich mit der Aufnahme dentaler Pathologien an Skelettmaterial eines frühmittelalterlichen Gräberfelds aus dem Bösfeld in Mannheim. Hierbei werden die Individuen in Hinblick auf AMTL, PMTL, Karies, marginale Parodontopathien, periapikale Läsionen, Zahnabnutzung, Zahnstein und Hypoplasien untersucht. In Folge werden die Häufigkeit der Pathologien innerhalb verschiedener Untergruppen der Bösfelder Population und zwischen anderen zeitgleichen und rezenten Populationen verglichen.rnrnBei der Prävalenz von AMTL und Karies ist ein signifikanter Anstieg mit dem Alter der Individuen zu beobachten, während sich kein Unterschied zwischen den Geschlechtern ergibt. Marginale Parodontopathien sind signifikant weniger bei frühadulten Individuen zu finden als bei der Gruppe der über 30 Jährigen. In der Gesamtpopulation ergeben sich keine Unterschiede zwischen den Geschlechtern. Altersabhängig betrachtet sind jedoch die über 40-jährigen Männer signifikant häufiger von marginalen Parodontopathien betroffen, während bei der Altersgruppe der Frühadulten die weiblichen Individuen häufiger betroffen sind. Unabhängig von Geschlecht und Alter kann bei den marginalen Parodontopathien ein Zusammenhang zwischen den alveolaren Entzündungsreaktionen und dem Abstand zwischen Schmelz-Zement Grenze und Limbus alveolaris festgestellt werden. Die männlichen Individuen des Bösfelds sind signifikant häufiger von periapikalen Läsionen betroffen. Bei dem Zahnverschleiß wird ein solcher Unterschied zwischen den Geschlechtern nicht festgestellt. Lediglich eine Zunahme des Verschleißes mit dem Alter liegt vor. Auch der Zahnsteinbefall steigt mit dem Alter an. Ein Unterschied bei dem Zahnsteinvorkommen zwischen den Geschlechtern ist nicht zu finden. Nur die frühmaturen Männer zeigen im Vergleich zu den Frauen einen signifikant geringeren Befall. Diese höhere Zahnsteinablagerung bei den frühmaturen Frauen kann mit deren Eintritt in das Klimakterium erklärt werden. Die Hypoplasien des Enamels lassen ein durchschnittliches Entstehungsalter von 3 bis 4 Jahren erkennen. Dieses kann mit dem, im Frühmittelalter sehr späten, Abstillalter in Verbindung gebracht werden. Die an der Bösfelder Serie beobachteten Häufigkeiten der Patholgien sind zu einem großen Teil vergleichbar mit anderen zeitgleichen Skelettserien. rnrnDie vorliegende Studie gibt einen Einblick in die Epidemiologie dentaler Pathologien im Frühmittelalter, kann Rückschlüsse ziehen auf damalige Lebensumstände und kann Unterschiede zwischen damaliger und heutiger Prävalenz verschiedener Erkrankungen darstellen. Zukünftige Studien an der Bösfelder Skelettserie können mit einem Fokus auf die archäologische Auswertung der Grabbeigaben weitere Erkenntnisse liefern und so das Verständnis dieser merowingerzeitlichen Population vertiefen. rn

Spatial computing per smart devices

Magic Carpet, nato come un middleware orientato a una dimostrazione sullo spatial computing, che inizialmente coinvolgeva solo smart devices ed un tappeto di tag NFC, è il punto di partenza per uno studio sulle tecnologie abilitanti in tale campo. Il prodotto finale è una toolchain per lo sviluppo e la distribuzione, su dispositivi connessi, di applicazioni di spatial computing. Essa comprende un interprete per un DSL basato su un core calculus formalizzato, Field Calculus, e un middleware che supporta l'astrazione curando, a basso livello, le comunicazioni con il vicinato e le percezioni ambientali.

Stochastic foundations of dynamic trade and labor market models

This dissertation consists of three self-contained papers that are related to two main topics. In particular, the first and third studies focus on labor market modeling, whereas the second essay presents a dynamic international trade setup.rnrnIn Chapter "Expenses on Labor Market Reforms during Transitional Dynamics", we investigate the arising costs of a potential labor market reform from a government point of view. To analyze various effects of unemployment benefits system changes, this chapter develops a dynamic model with heterogeneous employed and unemployed workers.rn rnIn Chapter "Endogenous Markup Distributions", we study how markup distributions adjust when a closed economy opens up. In order to perform this analysis, we first present a closed-economy general-equilibrium industry dynamics model, where firms enter and exit markets, and then extend our analysis to the open-economy case.rn rnIn Chapter "Unemployment in the OECD - Pure Chance or Institutions?", we examine effects of aggregate shocks on the distribution of the unemployment rates in OECD member countries.rn rnIn all three chapters we model systems that behave randomly and operate on stochastic processes. We therefore exploit stochastic calculus that establishes clear methodological links between the chapters.

Aggregate Programming in Scala: a Core Library and Actor-Based Platform for Distributed Computational Fields

La programmazione aggregata è un paradigma che supporta la programmazione di sistemi di dispositivi, adattativi ed eventualmente a larga scala, nel loro insieme -- come aggregati. L'approccio prevalente in questo contesto è basato sul field calculus, un calcolo formale che consente di definire programmi aggregati attraverso la composizione funzionale di campi computazionali, creando i presupposti per la specifica di pattern di auto-organizzazione robusti. La programmazione aggregata è attualmente supportata, in modo più o meno parziale e principalmente per la simulazione, da DSL dedicati (cf., Protelis), ma non esistono framework per linguaggi mainstream finalizzati allo sviluppo di applicazioni. Eppure, un simile supporto sarebbe auspicabile per ridurre tempi e sforzi d'adozione e per semplificare l'accesso al paradigma nella costruzione di sistemi reali, nonché per favorire la ricerca stessa nel campo. Il presente lavoro consiste nello sviluppo, a partire da un prototipo della semantica operazionale del field calculus, di un framework per la programmazione aggregata in Scala. La scelta di Scala come linguaggio host nasce da motivi tecnici e pratici. Scala è un linguaggio moderno, interoperabile con Java, che ben integra i paradigmi ad oggetti e funzionale, ha un sistema di tipi espressivo, e fornisce funzionalità avanzate per lo sviluppo di librerie e DSL. Inoltre, la possibilità di appoggiarsi, su Scala, ad un framework ad attori solido come Akka, costituisce un altro fattore trainante, data la necessità di colmare l'abstraction gap inerente allo sviluppo di un middleware distribuito. Nell'elaborato di tesi si presenta un framework che raggiunge il triplice obiettivo: la costruzione di una libreria Scala che realizza la semantica del field calculus in modo corretto e completo, la realizzazione di una piattaforma distribuita Akka-based su cui sviluppare applicazioni, e l'esposizione di un'API generale e flessibile in grado di supportare diversi scenari.

Influence of the condition of the adjacent tooth surface on fluorescence measurements for the detection of approximal caries

The aim of this study was to test whether the status of the adjacent tooth surface has an influence on the signal of a new laser fluorescence (LF) device for the detection of approximal caries. Seventy-eight teeth were selected from a pool of extracted permanent human molars, frozen at -20 degrees C until use. Before being measured the teeth were defrosted, cleaned, and any calculus removed. As a control, a defined approximal surface of each tooth was measured with the LF device holding the tip with the detecting- and the reverse-side on it, but without a neighboring tooth contacting the surface. The proximal site under examination was then placed adjacent to a tooth, which had deep dentinal caries, a composite restoration, a provisional ZnO-Eugenol restoration, or a ceramic restoration. The adjacent tooth with the ZnO-Eugenol restoration, the composite restoration, and the dentinal caries all demonstrated a statistically significant increase of LF readings on sound tooth surfaces. Teeth with enamel or dentinal caries were only slightly (and not statistically significantly) influenced by the different types of neighboring surfaces compared with the control LF readings. It can be concluded that caries detection of approximal tooth surfaces with the new LF system might be influenced by the condition of the adjacent tooth surface.

Detection of approximal caries with a new laser fluorescence device

The laser device DIAGNOdent developed for the detection of occlusal caries has limited value on approximal surfaces. The aim of this study was to develop and to test a new laser fluorescence (LF) device for the detection of approximal caries. Light with a wavelength of 655 nm was transported to the approximal surface using two different sapphire fibre tips. Seventy-five teeth were selected from a pool of extracted permanent human molars, frozen at -20 degrees C until use. Before being measured, they were defrosted, cleaned and calculus was removed with a scaler. The molars were set in blocks simulating the contact area of adults. Bitewing radiographs were obtained using Kodak Insight films. After two independent assessments with the new LF device, the teeth were histologically prepared, and assessed for caries extension. Using the laser, specificity values for D1 threshold (outer half of enamel), D2 threshold (inner half of enamel), D3 threshold (dentine) ranged between 0.81 and 0.93, sensitivity between 0.84 and 0.92 with no difference between the two tips. Bitewing radiography showed an inferior performance compared to LF (p<0.05). Intraex aminer reproducibility was high (kappa>.74). The new LF system might be a useful additional tool in detecting approximal caries. Because of its good reproducibility, it could be used to monitor caries regression or progression on approximal surfaces.

Renal oxygenation changes during acute unilateral ureteral obstruction: assessment with blood oxygen level-dependent mr imaging--initial experience

PURPOSE: To prospectively determine if changes in intrarenal oxygenation during acute unilateral ureteral obstruction can be depicted with blood oxygen level-dependent (BOLD) magnetic resonance (MR) imaging. MATERIALS AND METHODS: The study was approved by the local ethics committee, and written informed consent was obtained from all patients. BOLD MR imaging was performed in 10 male patients (mean age, 45 years +/- 17 [standard deviation]; range, 20-73 years) with a distal unilateral ureteral calculus and in 10 healthy age-matched male volunteers to estimate R2*, which is inversely related to tissue Po(2). R2* values were determined in the cortex and medulla of the obstructed and the contralateral nonobstructed kidneys. To reduce external effects on R2*, the R2* ratio between the medulla and cortex was also analyzed. Statistical analysis was performed with nonparametric rank tests. P < .05 was considered to indicate a significant difference. RESULTS: All patients had significantly lower medullary and cortical R2* values in the obstructed kidney (median R2* in medulla, 10.9 sec(-1) [range, 9.1-14.3 sec(-1)]; median R2* in cortex, 10.4 sec(-1) [range, 9.7-11.3 sec(-1)]) than in the nonobstructed kidney (median R2* in medulla, 17.2 sec(-1) [range, 14.6-23.2 sec(-1)], P = .005; median R2* in cortex, 11.7 sec(-1) [range, 11.0-14.0 sec(-1)], P = .005); values in the obstructed kidneys were also significantly lower than values in the kidneys of healthy control subjects (median R2* in medulla, 16.1 sec(-1) [range, 13.9-18.1 sec(-1)], P < .001; median R2* in cortex, 11.6 sec(-1) [range, 10.5-12.9 sec(-1)], P < .001). R2* ratios in the obstructed kidneys (median, 1.06; range, 0.85-1.27) were significantly lower than those in the nonobstructed kidneys (median, 1.49; range, 1.26-1.71; P = .005) and those in the kidneys of healthy control subjects (median, 1.38; range, 1.23-1.47; P < .001). In contrast, R2* ratios in the nonobstructed kidneys of patients were significantly higher than those in kidneys of healthy control subjects (P = .01). CONCLUSION: Increased oxygen content in the renal cortex and medulla occurs with acute unilateral ureteral obstruction, suggesting reduced function of the affected kidney.

Noninvasive assessment of acute ureteral obstruction with diffusion-weighted MR imaging: a prospective study

PURPOSE: To prospectively assess the potential of noninvasive diffusion-weighted magnetic resonance (MR) imaging to depict changes in microperfusion and diffusion in patients with acute unilateral ureteral obstruction. MATERIALS AND METHODS: The local ethics committee approved the study protocol. Informed consent was obtained. Diffusion-weighted MR imaging was performed in 21 patients (two women, 19 men; mean age, 43 years +/- 10 [standard deviation]) with acute unilateral ureteral obstruction due to a calculus diagnosed at unenhanced computed tomography. A control group (one woman, 15 men; mean age, 44 years +/- 12) underwent the same MR protocol. Standard processing yielded an apparent diffusion coefficient (ADC) ADCT; the separation of microperfusion and diffusion contributions yielded the perfusion fraction FP and the pure diffusion coefficient ADCD. ADCT, ADCD, and FP were compared between obstructed and contralateral unobstructed kidneys and with control values. For statistical analysis, nonparametric rank tests were used. A P value of less than .05 was considered significant. RESULTS: No significant differences were observed between the ADCT of the medulla or cortex of the obstructed and unobstructed kidneys. Compared with control kidneys, only medullary ADCT was slightly increased in the obstructed kidney (P < .04). However, the ADCD in the medulla of the obstructed and unobstructed kidneys was significantly higher than that in control subjects (201 x 10(-5) mm2/sec +/- 16 and 199 x 10(-5) mm2/sec +/- 20 vs 189 x 10(-5) mm2/sec +/- 12; P < .008 and P < .03, respectively). FP of the cortex of the obstructed kidney was significantly lower than that in the unobstructed kidney (20.2% +/- 4.8 vs 24.0% +/- 5.8; P < .002); FP of the medulla was slightly lower in the obstructed kidney than in the unobstructed kidney (18.3% +/- 5.9 vs 20.7% +/- 6.4; P = .05). CONCLUSION: Diffusion-weighted MR imaging allows noninvasive detection of changes in renal perfusion and diffusion during acute unilateral ureteral obstruction, as exemplified in patients with a ureteral calculus.

Tax-Optimal Step-Up and Imperfect Loss Offset

In the field of mergers and acquisitions, German and international tax law allow for several opportunities to step up a firm's assets, i.e., to revaluate the assets at fair market values. When a step-up is performed the taxpayer recognizes a taxable gain, but also obtains tax benefits in the form of higher future depreciation allowances associated with stepping up the tax base of the assets. This tax-planning problem is well known in taxation literature and can also be applied to firm valuation in the presence of taxation. However, the known models usually assume a perfect loss offset. If this assumption is abandoned, the depreciation allowances may lose value as they become tax effective at a later point in time, or even never if there are not enough cash flows to be offset against. This aspect is especiallyrelevant if future cash flows are assumed to be uncertain. This paper shows that a step-up may be disadvantageous or a firm overvalued if these aspects are not integrated into the basic calculus. Compared to the standard approach, assets should be stepped up only in a few cases and - under specific conditions - at a later point in time. Firm values may be considerably lower under imperfect loss offset.