Gerardo Schneider's Publications: Journals

[1] John J. Camilleri and Gerardo Schneider. Modelling and analysis of normative documents. Journal of Logical and Algebraic Methods in Programming, 91:33-59, October 2017. [ bib | DOI | http | .pdf ]
We are interested in using formal methods to analyse normative documents or contracts such as terms of use, privacy policies, and service agreements. We begin by modelling such documents in terms of obligations, permissions and prohibitions of agents over actions, restricted by timing constraints and including potential penalties resulting from the non-fulfilment of clauses. This is done using the C-O Diagram formalism, which we have extended syntactically and for which we have defined a new trace semantics. Models in this formalism can then be translated into networks of timed automata, and we have a complete working implementation of this translation. The network of automata is used as a specification of a normative document, making it amenable to verification against given properties. By applying this approach to a case study from a real-world contract, we show the kinds of analysis possible through both syntactic querying on the structure of the model, as well as verification of properties using Uppaal.

[2] Raúl Pardo, Musard Balliu, and Gerardo Schneider. Formalising privacy policies in social networks. Journal of Logical and Algebraic Methods in Programming, 90:125-157, August 2017. [ bib | DOI | http | .pdf ]
Social Network Services (SNS) have changed the way people communicate, bringing many benefits but also new concerns. Privacy is one of them. We present a framework to write privacy policies for {SNSs} and to reason about such policies in the presence of events making the network evolve. The framework includes a model of SNSs, a logic to specify properties and to reason about the knowledge of the users (agents) of the SNS, and a formal language to write privacy policies. Agents are enhanced with a reasoning engine allowing the inference of knowledge from previously acquired knowledge. To describe the way {SNSs} may evolve, we provide operational semantics rules which are classified into four categories: epistemic, topological, policy, and hybrid, depending on whether the events under consideration change the knowledge of the SNS' users, the structure of the social graph, the privacy policies, or a combination of the above, respectively. We provide specific rules for describing Twitter's behaviour, and prove that it is privacy-preserving (i.e., that privacy is preserved under every possible event of the system). We also show how Twitter and Facebook are not privacy-preserving in the presence of additional natural privacy policies.

[3] Wolfgang Ahrendt, Mauricio Chimento, Gordon Pace, and Gerardo Schneider. Verifying Data- and Control-Oriented Properties Combining Static and Runtime Verification: Theory and Tools. Formal Methods in System Design, 51(1):200-265, August 2017. [ bib | DOI | .pdf ]
Static verification techniques are used to analyse and prove properties about programs before they are executed. Many of these techniques work directly on the source code and are used to verify data-oriented properties over all possible executions. The analysis is necessarily an over-approximation as the real executions of the program are not available at analysis time. In contrast, runtime verification techniques have been extensively used for control-oriented properties, analysing the current execution path of the program in a fully automatic manner. In this article, we present a novel approach in which data-oriented and control-oriented properties may be stated in a single formalism amenable to both static and dynamic verification techniques. The specification language we present to achieve this that of ppDATEs, which enhances the control-oriented property language of DATEs, with data-oriented pre/postconditions. For runtime verification of ppDATE specifications, the language is translated into a DATE. We give a formal semantics to ppDATEs, which we use to prove the correctness of our translation from ppDATEs to DATEs. We show how ppDATE specifications can be analysed using a combination of the deductive theorem prover KeY and the runtime verification tool LARVA. Verification is performed in two steps: KeY first partially proves the data-oriented part of the specification, simplifying the specification which is then passed on to LARVA to check at runtime for the remaining parts of the specification including the control-oriented aspects. We show the applicability of our approach on two case studies.

[4] Shaun Azzopardi, Gordon J. Pace, Fernando Schapachnik, and Gerardo Schneider. Contract Automata: An Operational View of Contracts Between Interactive Parties. Artificial Intelligence and Law, 24(3):203-243, September 2016. [ bib | DOI | .pdf ]
Deontic logic as a way of formally reasoning about norms, an important area in AI and law, has traditionally concerned itself about formalising provisions of general statutes. Despite the long history of deontic logic, given the wide scope of the logic, it is difficult, if not impossible, to formalise all these notions in a single formalism, and there are still ongoing debates on appropriate semantics for deontic modalities in different contexts. In this paper, we restrict our attention to contracts between interactive parties, which are both general enough to be an interesting object of study but specific enough so as to narrow down the debates regarding the meaning of modalities, and present a formalism for reasoning about them.

[5] Gregorio Díaz, M. Emilia Cambronero, Enrique Martínez, and Gerardo Schneider. Specification and Verification of Normative texts using C-O Diagrams. IEEE Transactions on Software Engineering, 40(8):795-817, 2014. [ bib | DOI | .pdf ]
C-O Diagrams have been introduced as a means to have a more visual representation of normative texts and electronic contracts, where it is possible to represent the obligations, permissions and prohibitions of the different signatories, as well as the penalties resulting from non-fulfillment of their obligations and prohibitions. In such diagrams we are also able to represent absolute and relative timing constraints. In this paper we present a formal semantics for C-O Diagrams based on timed automata extended with information regarding the satisfaction and violation of clauses in order to represent different deontic modalities. As a proof of concept, we apply our approach to two different case studies, where the method presented here has successfully identified problems in the specification.

[6] Krasimir Angelov, John J. Camilleri, and Gerardo Schneider. A framework for conflict analysis of normative texts written in controlled natural language. Journal of Logic and Algebraic Programming, 82(5-7):216-240, July-October 2013. [ bib | DOI | .pdf ]
In this paper we are concerned with the analysis of normative conflicts, or the detection of conflicting obligations, permissions and prohibitions in normative texts written in a Controlled Natural Language (CNL). For this we present , a proof-of-concept system where normative texts written in CNL are automatically translated into the formal language CL using the Grammatical Framework (GF). Such CL expressions are then analysed for normative conflicts by the CLAN tool, which gives counter-examples in cases where conflicts are found. The framework also uses GF to give a CNL version of the counter-example, helping the user to identify the conflicts in the original text. We detail the application of AnaCon to two case studies and discuss the effectiveness of our approach.

[7] Hallstein Hansen, Gerardo Schneider, and Martin Steffen. Reachability analysis of complex planar hybrid systems. Science of Computer Programming (SCP), 78(12):2511-2536, 2013. [ bib | DOI | .pdf ]
Hybrid systems are systems that exhibit both discrete and continuous behavior. Reachability, the question of whether a system in one state can reach some other state, is undecidable for hybrid systems in general. The Generalized Polygonal Hybrid System (GSPDI) is a restricted form of hybrid automaton where reachability is decidable. It is limited to two continuous variables that uniquely determine which location the automaton is in, and restricted in that the discrete transitions does not allow changes in the state, only the location, of the automaton. One application of GSPDIs is for approximating control systems and verifying the safety of such systems. In this paper we present the following two contributions: i) An optimized algorithm that answers reachability questions for GSPDIs, where all cycles in the reachability graph are accelerated. ii) An algorithm by which more complex planar hybrid systems are over-approximated by GSPDIs subject to two measures of precision. We prove soundness, completeness, and termination of both algorithms, and discuss their implementation.

[8] Cristian Prisacariu and Gerardo Schneider. A dynamic deontic logic for complex contracts. Journal of Logic and Algebraic Programming, 81(4):458-490, May 2012. [ bib | DOI | .pdf ]
We present a dynamic deontic logic for specifying and reasoning about complex contracts. The concepts that our contract logic CL captures are drawn from legal contracts, as we consider that these are more general and expressive that what is usually found in computer science (like in software contracts, web services specifications, or communication protocols). CL is intended to be used in specifying complex contracts found in computer science. This influences many of the design decisions behind CL. We adopt an ought-to-do approach to deontic logic and apply the deontic modalities exclusively over complex actions. We add the dynamic logic modality so to be able to reason about what happens after an action is performed. CL can reason about regular synchronous actions done at the same time. CL incorporates the notions of contrary-to-duty and contrary-to-prohibition by attaching to the deontic modalities explicitly a reparation which is to be enforced in case of violations. Results of decidability and tree model property are given as well as specific properties for the modalities.

[9] Eugene Asarin, Venkatesh Mysore, Amir Pnueli, and Gerardo Schneider. Low dimensional hybrid systems - decidable, undecidable, don't know. Information and Computation, 211:138-159, January 2012. [ bib | DOI | .pdf ]
Even though many attempts have been made to define the boundary between decidable and undecidable hybrid systems, the affair is far from being solved. More and more low dimensional systems are being shown to be undecidable with respect to reachability, and many open problems in between are being discovered. In this paper, we present various two dimensional hybrid systems for which the reachability problem is undecidable. We show their undecidability by simulating Minsky machines. Their proximity to the decidability frontier is understood by inspecting the most parsimonious constraints necessary to make reachability over these automata decidable. We also show that for other two dimensional systems, the reachability question remains unanswered, by proving that it is as hard as the reachability problem for piecewise affine maps on the real line, which is a well known open problem.

[10] Eugene Asarin, Gordon Pace, Gerardo Schneider, and Sergio Yovine. Algorithmic Analysis of Polygonal Hybrid Systems. Part II: Phase Portrait and Tools. Theoretical Computer Science, 390(1):1-26, January 2008. [ bib | DOI | .pdf ]
Polygonal differential inclusion systems (SPDI) are a subclass of planar hybrid automata which can be represented by piecewise constant differential inclusions. The reachability problem as well as the computation of certain objects of the phase portrait is decidable. In this paper we show how to compute the viability, controllability and invariance kernels, as well as semi-separatrix curves for SPDIs. We also present the tool SPeeDI+, which implements a DFS reachability algorithm and the phase portrait computation for SPDIs.

[11] Eugene Asarin, Gerardo Schneider, and Sergio Yovine. Algorithmic Analysis of Polygonal Hybrid Systems. Part I: Reachability. Theoretical Computer Science, 379(1-2):231-265, 2007. [ bib | DOI | .pdf ]
In this work we are concerned with the formal verification of two-dimensional non-deterministic hybrid systems, namely polygonal differential inclusion systems (SPDIs). SPDIs are a class of nondeterministic systems that correspond to piecewise constant differential inclusions on the plane, for which we study the reachability problem. Our contribution is the development of an algorithm for solving exactly the reachability problem of SPDIs. We extend the geometric approach due to Maler and Pnueli to non-deterministic systems, based on the combination of three techniques: the representation of the two-dimensional continuous-time dynamics as a one-dimensional discrete-time system (using Poincaré maps), the characterization of the set of qualitative behaviors of the latter as a finite set of types of signatures, and acceleration used to explore reachability according to each of these types.

[12] Gerardo Schneider. Computing invariance kernels of polygonal hybrid systems. Nordic Journal of Computing, 11(2):194-210, 2004. [ bib | .pdf ]
Polygonal hybrid systems are a subclass of planar hybrid automata which can be represented by piecewise constant differential inclusions. One way of analysing such systems (and hybrid systems in general) is through the study of their phase portrait, which characterise the systems' qualitative behaviour. In this paper we identify and compute an important object of polygonal hybrid systems' phase portrait, namely invariance kernels. An invariant set is a set of points such that any trajectory starting in such point keep necessarily rotating in the set forever and the invariance kernel is the largest of such sets. We show that this kernel is a non-convex polygon and we give a non-iterative algorithm for computing the coordinates of its vertexes and edges. Moreover, we show some properties of such systems' simple cycles.


This file was generated by bibtex2html 1.97.