@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}}
@article{AJPS23abe,
author = {Hamed Arshad and
Christian Johansen and
Pablo Picazo{-}Sanchez and
Gerardo Schneider},
title = {Attribute-Based Encryption with Enforceable Obligations},
journal = {Journal of Cryptographic Engineering},
year = {2023},
volume = {13},
number = {3},
pages = {343--371},
abstract = {Attribute-Based Encryption (ABE) is a cryptographic mechanism that provides fine-grained access control to encrypted data, which can thus be stored in, e.g., public clouds. However, ABE schemes lack the notion of obligations, which is common in Attribute-Based Access Control systems such as eXtensible Access Control Markup Language and Usage Control. Obligations are used to define and enforce extra constraints that happen before approving or denying an access request. In this paper, we propose Attribute-Based Encryption with enforceable OBligations (OB-ABE), a system for extending any classical ABE with enforceable obligations. Our system architecture has as core component trusted hardware enclaves, implemented with Intel Software Guard Extensions (SGX), used for enforcing obligations. We employ ProVerif to formally model OB-ABE and verify its main property called ``enforceable obligations’’, i.e., if a message is encrypted along with an obligation, then the message can be decrypted only after enforcing the attached obligation. OB-ABE has two more properties: (i) OB-ABE is a ``conservative extension’’ of the underlying ABE scheme, preserving its security properties; (ii) OB-ABE is ``backward compatible’’ in the sense that any ciphertext produced by an ABE scheme can be decrypted by its extended OB-ABE version, and moreover, a ciphertext produced by an OB-ABE scheme can be decrypted by its underlying ABE scheme provided that the ciphertext does not have obligations attached.
We also implement in C using Intel SGX a prototype of an OB-ABE extending the well-known Ciphertext-Policy ABE.},
pdf = {JCE2023.pdf},
doi = {10.1007/s13389-023-00317-1}
}
@article{PSS22ace,
author = {Pablo Picazo{-}Sanchez and
Lara Ortiz{-}Martin and
Gerardo Schneider and
Andrei Sabelfeld},
title = {Are chrome extensions compliant with the spirit of least privilege?},
journal = {International Journal of Information Security},
volume = {21},
number = {6},
pages = {1283--1297},
year = {2022},
url = {https://doi.org/10.1007/s10207-022-00610-w},
doi = {10.1007/s10207-022-00610-w},
abstract = {Extensions are small applications installed by users and enrich the user experience of browsing the Internet. Browsers expose a set of restricted APIs to extensions. To be used, extensions need to list the permissions associated with these APIs in a mandatory extension file named manifest. In particular, Chrome’s permission ecosystem was designed in the spirit of the least privilege. Yet, this paper demonstrates that 39.8\% of the analyzed extensions provided by the official Web Store are compliant with the spirit of least privilege. Also, we develop: (1) a browser extension to make aware regular users of the permissions the extensions they install; (2) a web app where extensions developers can check whether their extensions are compliant with the spirit of the least privileged; and (3) a set of scripts that can be part of the vendors’ acceptance criteria such that when developers upload their extensions to the official repositories, the scripts automatically analyze the extensions and generate a report about the permissions and the usage.},
pdf = {}
}
@article{HMR+22csm,
author = {William Hughes and Tobias Magnusson and Alejandro Russo and Gerardo Schneider},
title = {Cheap and secure metatransactions on the blockchain using hash-based authorisation and preferred batchers},
journal = {Blockchain: Research and Applications},
publisher = {Elsevier},
year = {2022},
issn = {2096-7209},
optkey = {},
optvolume = {},
optnumber = {},
optpages = {},
month = {December},
note = {In Press, available online},
doi = {10.1016/j.bcra.2022.100125},
keywords = {Ethereum, Domain-specific language, Interpreter, Gas optimisation},
abstract = {Smart contracts are self-executing programs running in the blockchain allowing for decentralised storage and execution without a middleman. On-chain execution is expensive, with miners charging fees for distributed execution according to a cost model defined in the protocol. In particular, transactions have a high fixed cost. We present MultiCall, a transaction-batching interpreter for Ethereum that reduces the cost of smart contract executions by gathering multiple users’ transactions into a batch. Our current implementation of MultiCall includes the following features: the ability to emulate Ethereum call and create transactions, both from MultiCall itself and using an identity unique to the user; the ability to cheaply pay ether to other MultiCall users; and the ability to authorise emulated transactions on behalf of multiple users in a single transaction using hash-based authorisation rather than more expensive signatures. This improves upon on a previous version of MultiCall. Our experiments show that MultiCall provides a saving between 57\% and 99\% of the fixed transaction cost compared with the standard approach of sending Ethereum transactions directly. Besides, we also show how to prevent an economic attack exploiting the metatransaction feature, describe a generic protocol for hash-based authorisation of metatransactions, and analyse how to minimise its off-chain computational and storage cost.},
pdf = {}
}
@article{AJO+22sab,
author = {Hamed Arshad and
Christian Johansen and
Olaf Owe and
Pablo Picazo{-}Sanchez and
Gerardo Schneider},
title = {Semantic Attribute-Based Encryption: {A} framework for combining {ABE} schemes with semantic technologies},
journal = {Information Sciences},
volume = {616},
pages = {558--576},
year = {2022},
url = {https://doi.org/10.1016/j.ins.2022.10.132},
doi = {10.1016/j.ins.2022.10.132},
abstract = {Attribute-Based Encryption (ABE) is a cryptographic solution to protect resources in a fine-grained manner based on a set of public attributes. This is similar to attribute-based access control schemes in the sense that both rely on public attributes and access control policies to grant access to resources. However, ABE schemes do not consider the semantics of attributes provided by users or required by access structures. Such semantics not only improve the functionality by making proper access decisions but also enable cross-domain interoperability by making users from one domain able to access and use resources of other domains. This paper proposes a Semantic ABE (SABE) framework by augmenting a classical Ciphertext-Policy ABE (CP-ABE) scheme with semantic technologies using a generic procedure by which any CP-ABE scheme can be extended to an SABE. The proposed SABE framework is implemented in Java and the source code is publicly available. The experiment results confirm that the performance of the proposed framework is promising.},
pdf = {}
}
@article{JPF+22mdpl,
author = {Johanna Johansen and
Tore Pedersen and
Simone Fischer{-}H{\"{u}}bner and
Christian Johansen and
Gerardo Schneider and
Arnold Roosendaal and
Harald Zwingelberg and
Anders Jakob Sivesind and
Josef Noll},
title = {A multidisciplinary definition of privacy labels},
journal = {Inf. Comput. Secur.},
volume = {30},
number = {3},
pages = {452--469},
year = {2022},
opturl = {https://doi.org/10.1108/ICS-06-2021-0080},
doi = {10.1108/ICS-06-2021-0080},
pdf = {ICS2022.pdf},
abstract = {Privacy is currently in distress and in need of rescue, much like princesses in the allfamiliar fairytales. We employ storytelling and metaphors from fairytales to make reader-friendly and streamline our arguments about how a complex concept of Privacy Labeling (the ‘knight in shining armor’) can be a solution to the current state of Privacy (the ‘princess in distress’). We give a precise definition of Privacy Labeling (PL), painting a panoptic portrait from seven different perspectives (the ‘seven helpers’): Business, Legal, Regulatory, Usability and Human Factors, Educative, Technological, and Multidisciplinary. We describe a common vision, proposing several important ‘traits of character’ of PL as well as identifying ‘undeveloped potentialities’, i.e., open problems on which the community can focus. More specifically, this position paper identifies the stakeholders of the PL and their needs with regard to privacy, describing how PL should be and look like in order to address these needs. Throughout the paper, we highlight goals, characteristics, open problems, and starting points for creating, what we consider to be, the ideal PL. In the end we present three approaches to establish and manage PL, through: self-evaluations, certifications, or community endeavors. Based on these, we sketch a roadmap for future developments.}
}
@article{SSS+21gbm,
author = {Stucki, Sandro and S{\'a}nchez, C{\'e}sar and Schneider, Gerardo and Bonakdarpour, Borzoo},
doi = {10.1007/s10703-020-00358-w},
isbn = {1572-8102},
journal = {Formal Methods in System Design},
title = {Gray-box monitoring of hyperproperties with an application to privacy},
volume = {58},
number = {1-2},
pages = {126--159},
url = {https://doi.org/10.1007/s10703-020-00358-w},
year = {2021},
abstract = {Runtime verification is a complementary approach to testing, model checking and other static verification techniques to verify software properties. Monitorability characterizes what can be verified (monitored) at run time. Different definitions of monitorability have been given both for trace properties and for hyperproperties (properties defined over sets of traces), but these definitions usually cover only some aspects of what is important when characterizing the notion of monitorability. The first contribution of this paper is a refinement of classic notions of monitorability both for trace properties and hyperproperties, taking into account, among other things, the computability of the monitor. A second contribution of our work is to show that black-box monitoring of HyperLTL (a logic for hyperproperties) is in general unfeasible, and to suggest a gray-box approach in which we combine static and runtime verification. The main idea is to call a static verifier as an oracle at run time allowing, in some cases, to give a final verdict for properties that are considered to be non-monitorable under a black-box approach. Our third contribution is the instantiation of this solution to a privacy property called distributed data minimization which cannot be verified using black-box runtime verification. We use an SMT-based static verifier as an oracle at run time. We have implemented our gray-box approach for monitoring data minimization into the proof-of-concept tool Minion. We describe the tool and apply it to a few case studies to show its feasibility.},
pdf = {}
}
@article{APP+20cac,
author = {Hanaa Alshareef and Ra{\'{u}}l Pardo and Pablo Picazo-Sanchez and Gerardo Schneider},
title = {A Collaborative Access Control Framework for Online Social Networks},
journal = {Journal of Logical and Algebraic Methods in Programming},
volume = {114},
pages = {},
month = {May},
year = {2020},
url = {https://doi.org/10.1016/j.jlamp.2020.100562},
doi = {10.1016/j.jlamp.2020.100562},
issn = {2352-2208},
abstract = {Most Online Social Networks allow users to set their privacy settings concerning posting information, but current implementations do not allow a fine grained enforcement in case the posted item concerns other users. In this paper we propose a new collaborative access control framework that takes into account the relation of multiple users for viewing as well as for sharing items, eventually solving conflicts in the privacy settings of the users involved. Our solution relies on two algorithms, one for viewing and another one for sharing items. We provide an evaluation of these algorithms where we demonstrate how varying some of the parameters directly influences the decision of viewing or sharing an item. Last but not least, we present a proof-of-concept implementation of our approach in an open source social network called Diaspora.},
pdf = {jlamp2020.pdf}
}
@article{PTS20ayp,
author = {Pablo Picazo{-}Sanchez and
Juan Tapiador and
Gerardo Schneider},
title = {After You, Please: Browser Extensions Order Attacks and Countermeasures},
journal = {International Journal of Information Security},
optjournal = {Int. J. Inf. Sec.},
volume = {19},
number = {6},
pages = {623--638},
year = {2020},
url = {https://doi.org/10.1007/s10207-019-00481-8},
doi = {10.1007/s10207-019-00481-8},
abstract = {Browser extensions are small applications executed in the browser context that provide additional capabilities and enrich the user experience while surfing the web. The acceptance of extensions in current browsers is unquestionable. For instance, Chrome's official extension repository has more than 63,000 extensions, with some of them having more than 10M users. When installed, extensions are pushed into an internal queue within the browser. The order in which each extension executes depends on a number of factors, including their relative installation times. In this paper, we demonstrate how this order can be exploited by an unprivileged malicious extension (i.e., one with no more permissions than those already assigned when accessing web content) to get access to any private information that other extensions have previously introduced. We propose a solution that does not require modifying the core browser engine, since it is implemented as another browser extension. We prove that our approach effectively protects the user against usual attackers (i.e., any other installed extension) as well as against strong attackers having access to the effects of all installed extensions (i.e., knowing who did what). We also prove soundness and robustness of our approach under reasonable assumptions.},
issn = {1615-5270},
pdf = {InfSec2020.pdf}
}
@article{OPP+19fai,
author = {Lara Ortiz{-}Martin and
Pablo Picazo{-}Sanchez and
Pedro Peris{-}Lopez and
Juan Tapiador and
Gerardo Schneider},
title = {Feasibility Analysis of Inter-Pulse Intervals Based Solutions for
Cryptographic Token Generation by Two Electrocardiogram Sensors},
journal = {Future Generation Comp. Syst.},
volume = {96},
pages = {283--296},
year = {2019},
url = {https://doi.org/10.1016/j.future.2019.02.021},
doi = {10.1016/j.future.2019.02.021},
abstract = {In this paper we address the problem of how two devices that are sensing the same heart signal can generate the same cryptographic token by extracting them from the Inter-Pulse Intervals (IPIs) of each cardiac signal. Our analysis is based on the use of a run-time monitor, which is extracted from a formal model and verified against predefined properties, combined with a fuzzy extractor to improve the final result. We first show that it is impossible, in general, to correct the differences between the IPIs derived from two captured electrocardiogram (ECG) signals when using only error correction techniques, thus being impossible to corroborate previous claims on the feasibility of this approach. Then, we provide a large-scale evaluation of the proposed method (run-time monitor and fuzzy extractor) over 19 public databases from the Physionet repository containing heart signals. The results clearly show the practicality of our proposal achieving a 91\% of synchronization probability for healthy individuals. Additionally, we also conduct an experiment to check how long the sensors should record the heart signal in order to generate tokens of 32, 64 and 128 bits. Contrarily to what it is usually assumed (6, 12, and 24 s for individuals with a heart rate of 80 beats-per-minute), the sensors have to wait 13, 28 and 56.5 s on median, respectively, to derive the same token from both sensors.},
pdf = {fgcs2019.pdf}
}
@article{SSA+19ASC,
author = {C\'esar S\'anchez and
Gerardo Schneider and
Wolfgang Ahrendt and
Ezio Bartocci and
Domenico Bianculli and
Christian Colombo and
Yli\'es Falcone and
Adrian Francalanza and
Srdan Krsti\'{c} and
Dejan Nickovic and
Gordon J.~Pace and
Jose Rufino and
Julien Signoles and
Dmitriy Traytel and
Alexander Weiss},
title = {{A Survey of Challenges for Runtime Verification from
Advanced Application Domains (Beyond Software)}},
journal = {Formal Methods in System Design},
year = {2019},
month = {August},
volume = {54},
number = {3},
pages = {279--335},
publisher = {Springer},
doi = {10.1007/s10703-019-00337-w},
optisbn = {},
e-issn = {1572-8102},
issn = {0925-9856},
note = {Open source, freely available at \url{https://rdcu.be/bOhjI}},
abstract = {Runtime verification is an area of formal methods that studies the
dynamic analysis of execution traces against formal specifications.
Typically, the two main activities in runtime verification efforts
are the process of creating monitors from specifications, and the
algorithms for the evaluation of traces against the generated
monitors.
Other activities involve the instrumentation of the system to
generate the trace and the communication between the system under
analysis and the monitor.
Most of the applications in runtime verification have been focused
on the dynamic analysis of software, even though there are many more
potential applications to other computational devices and target
systems.
In this paper we present a collection of challenges for runtime
verification extracted from concrete application domains, focusing
on the difficulties that must be overcome to tackle these specific
challenges.
The computational models that characterize these domains require to
devise new techniques beyond the current state of the art in runtime
verification.},
pdf = {fmsd2019.pdf}
}
@article{PBS17fpp,
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 = {https://doi.org/10.1016/j.jlamp.2017.02.008},
url = {http://www.sciencedirect.com/science/article/pii/S235222081730038X},
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}
}
@article{CS17man,
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 = {https://doi.org/10.1016/j.jlamp.2017.05.002},
url = {http://www.sciencedirect.com/science/article/pii/S2352220817300822},
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}
}
@article{ACP+17vdc,
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}
}
@article{APS+16ca,
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.
}
}
@article{DCM+13svn,
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 = {http://dx.doi.org/10.1109/TSE.2013.54},
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.}
}
@article{ACS13fca,
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 = {http://dx.doi.org/10.1016/j.jlap.2013.03.002}
}
@article{HSS11rac,
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 = {http://dx.doi.org/10.1016/j.scico.2013.02.007}
}
@article{PS12ddl,
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 = {http://dx.doi.org/10.1016/j.jlap.2012.03.003}
}
@article{AMP+12ldhs,
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 = {http://dx.doi.org/10.1016/j.ic.2011.11.006}
}
@article{APSY08tcs,
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 = {http://dx.doi.org/10.1016/j.tcs.2007.09.025}
}
@article{ASY07tcs1,
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 = {http://dx.doi.org/10.1016/j.tcs.2007.03.055}
}
@article{schneider04njc,
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 = {http://dx.doi.org/},
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.