@comment{{This file has been generated by bib2bib 1.97}}
@comment{{Command line: bib2bib -c '$type = "ARTICLE"' -ob my-publications-Journal.bib my-publications.bib}}
  author = {Ra\'ul Pardo and Musard Balliu and Gerardo Schneider},
  title = {Formalising Privacy Policies in Social Networks},
  journal = {Journal of Logical and Algebraic Methods in Programming},
  volume = {90},
  optnumber = {},
  pages = {125--157},
  month = {August},
  year = {2017},
  issn = {2352-2208},
  doi = {},
  url = {},
  abstract = {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.},
  pdf = {jlamp2017-privacy_policies.pdf}
  author = {John J. Camilleri and Gerardo Schneider},
  title = {Modelling and Analysis of Normative Documents},
  journal = {Journal of Logical and Algebraic Methods in Programming},
  volume = {91},
  optnumber = {},
  pages = {33--59},
  month = {October},
  year = {2017},
  issn = {2352-2208},
  doi = {},
  url = {},
  abstract = {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.},
  pdf = {jlamp2017-normative_doc.pdf}
  author = {Wolfgang Ahrendt and Mauricio Chimento and Gordon Pace and Gerardo Schneider},
  title = {{Verifying Data- and Control-Oriented Properties Combining Static and Runtime Verification: Theory and Tools}},
  journal = {Formal Methods in System Design},
  year = {2017},
  volume = {51},
  number = {1},
  pages = {200--265},
  month = {August},
  publisher = {Springer},
  doi = {10.1007/s10703-017-0274-y},
  isbn = {},
  e-issn = {1572-8102},
  issn = {0925-9856},
  abstract = {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.
  pdf = {fmsd2017.pdf}
  author = {Shaun Azzopardi and Gordon J.~Pace and Fernando Schapachnik and Gerardo Schneider},
  title = {{Contract Automata: An Operational View of Contracts Between Interactive Parties}},
  journal = {Artificial Intelligence and Law},
  year = {2016},
  volume = {24},
  number = {3},
  pages = {203--243},
  month = {September},
  publisher = {Springer},
  doi = {10.1007/s10506-016-9185-2},
  isbn = {},
  e-issn = {1572-8382},
  issn = {0924-8463},
  pdf = {arti2016.pdf},
  abstract = {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.
  author = {Gregorio D\'{i}az and M.~Emilia Cambronero and Enrique Mart\'{i}nez and Gerardo Schneider},
  doi = {10.1109/TSE.2013.54},
  issn = {0098-5589},
  journal = {IEEE Transactions on Software Engineering},
  number = {8},
  pages = {795-817},
  pdf = {tse2013.pdf},
  title = {{Specification and Verification of Normative texts using C-O Diagrams}},
  volume = {40},
  year = {2014},
  doi = {},
  abstract = {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.}
  abstract = {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 \AnaCon, 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.},
  author = {Krasimir Angelov and John J.~Camilleri and Gerardo Schneider},
  doi = {10.1016/j.jlap.2013.03.002},
  issn = {1567-8326},
  journal = {{Journal of Logic and Algebraic Programming}},
  month = {July-October},
  number = {5-7},
  pages = {216-240},
  pdf = {jlap13-CL_GF.pdf},
  publisher = {Elsevier},
  title = {A Framework for Conflict Analysis of Normative Texts Written in Controlled Natural Language},
  volume = {82},
  year = {2013},
  bdsk-url-1 = {}
  abstract = {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.},
  author = {Hallstein Hansen and Gerardo Schneider and Martin Steffen},
  doi = {10.1016/j.scico.2013.02.007},
  issn = {0167-6423},
  journal = {Science of Computer Programming (SCP)},
  number = {12},
  pages = {2511-2536},
  pdf = {scp2013.pdf},
  title = {Reachability analysis of complex planar hybrid systems},
  volume = {78},
  year = {2013},
  bdsk-url-1 = {}
  abstract = {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.},
  author = {Cristian Prisacariu and Gerardo Schneider},
  doi = {10.1016/j.jlap.2012.03.003},
  issn = {1567-8326},
  journal = {Journal of Logic and Algebraic Programming},
  month = {May},
  number = {4},
  pages = {458-490},
  pdf = {jlap2012.pdf},
  publisher = {Elsevier},
  title = {A Dynamic Deontic Logic for Complex Contracts},
  volume = {81},
  year = {2012},
  bdsk-url-1 = {}
  abstract = {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.},
  author = {Eugene Asarin and Venkatesh Mysore and Amir Pnueli and Gerardo Schneider},
  doi = {10.1016/j.ic.2011.11.006},
  issn = {0890-5401},
  journal = {Information and Computation},
  month = {January},
  optnote = {Submitted Jun 2009, Revised Jun 2011, Accepted Nov 2011, Final Version Dec 2011},
  pages = {138-159},
  pdf = {infcomp2012.pdf},
  publisher = {Elsevier},
  title = {Low Dimensional Hybrid Systems - Decidable, Undecidable, Don't Know},
  volume = {211},
  year = {2012},
  bdsk-url-1 = {}
  abstract = {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.},
  author = {Eugene Asarin and Gordon Pace and Gerardo Schneider and Sergio Yovine},
  doi = {10.1016/j.tcs.2007.09.025},
  issn = {0304-3975},
  journal = {Theoretical Computer Science},
  month = {January},
  number = {1},
  pages = {1--26},
  pdf = {tcs07-2.pdf},
  publisher = {Elsevier},
  title = {{Algorithmic Analysis of Polygonal Hybrid Systems. Part II: Phase Portrait and Tools}},
  volume = {390},
  year = {2008},
  bdsk-url-1 = {}
  abstract = {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\'e 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.
  author = {Eugene Asarin and Gerardo Schneider and Sergio Yovine},
  doi = {10.1016/j.tcs.2007.03.055},
  issn = {0304-3975},
  journal = {Theoretical Computer Science},
  number = {1-2},
  pages = {231--265},
  pdf = {tcs07.pdf},
  publisher = {Elsevier},
  title = {{Algorithmic Analysis of Polygonal Hybrid Systems. Part I: Reachability}},
  volume = {379},
  year = {2007},
  bdsk-url-1 = {}
  abstract = {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 {\em invariance kernels}. An \emph{invariant set} is a set of points such that any trajectory starting in such point keep necessarily rotating in the set forever and the \emph{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.
  author = {Gerardo Schneider},
  issn = {1236-6064},
  journal = {Nordic Journal of Computing},
  number = {2},
  opturl = {},
  pages = {194--210},
  pdf = {njc.pdf},
  title = {Computing Invariance Kernels of Polygonal Hybrid Systems},
  volume = {11},
  year = {2004}

This file was generated by bibtex2html 1.97.