Showing 1–22 of 22 results for author: Nielson, F

Experimental benchmarking of an automated deterministic error suppression workflow for quantum algorithms

Authors: Pranav S. Mundada, Aaron Barbosa, Smarak Maity, Yulun Wang, T. M. Stace, Thomas Merkh, Felicity Nielson, Andre R. R. Carvalho, Michael Hush, Michael J. Biercuk, Yuval Baum

Abstract: Excitement about the promise of quantum computers is tempered by the reality that the hardware remains exceptionally fragile and error-prone, forming a bottleneck in the development of novel applications. In this manuscript, we describe and experimentally test a fully autonomous workflow designed to deterministically suppress errors in quantum algorithms from the gate level through to circuit exec… ▽ More Excitement about the promise of quantum computers is tempered by the reality that the hardware remains exceptionally fragile and error-prone, forming a bottleneck in the development of novel applications. In this manuscript, we describe and experimentally test a fully autonomous workflow designed to deterministically suppress errors in quantum algorithms from the gate level through to circuit execution and measurement. We introduce the key elements of this workflow, delivered as a software package called Fire Opal, and survey the underlying physical concepts: error-aware compilation, automated system-wide gate optimization, automated dynamical decoupling embedding for circuit-level error cancellation, and calibration-efficient measurement-error mitigation. We then present a comprehensive suite of performance benchmarks executed on IBM hardware, demonstrating up to > 1000X improvement over the best alternative expert-configured techniques available in the open literature. Benchmarking includes experiments using up to 16 qubit systems executing: Bernstein Vazirani, Quantum Fourier Transform, Grover's Search, QAOA, VQE, Syndrome extraction on a five-qubit Quantum Error Correction code, and Quantum Volume. Experiments reveal a strong contribution of Non-Markovian errors to baseline algorithmic performance; in all cases the deterministic error-suppression workflow delivers the highest performance and approaches incoherent error bounds without the need for any additional sampling or randomization overhead, while maintaining compatibility with all additional probabilistic error suppression techniques. △ Less

Submitted 3 May, 2023; v1 submitted 14 September, 2022; originally announced September 2022.

Comments: 20 pages, 16 figures

Similarity Downselection: A Python implementation of a heuristic search algorithm for finding the set of the n most dissimilar items with an application in conformer sampling

Authors: Felicity F. Nielson, Sean M. Colby, Ryan S. Renslow, Thomas O. Metz

Abstract: Finding the set of the n items most dissimilar from each other out of a larger population becomes increasingly difficult and computationally expensive as either n or the population size grows large. Finding the set of the n most dissimilar items is different than simply sorting an array of numbers because there exists a pairwise relationship between each item and all other items in the population.… ▽ More Finding the set of the n items most dissimilar from each other out of a larger population becomes increasingly difficult and computationally expensive as either n or the population size grows large. Finding the set of the n most dissimilar items is different than simply sorting an array of numbers because there exists a pairwise relationship between each item and all other items in the population. For instance, if you have a set of the most dissimilar n=4 items, one or more of the items from n=4 might not be in the set n=5. An exact solution would have to search all possible combinations of size n in the population, exhaustively. We present an open-source software called similarity downselection (SDS), written in Python and freely available on GitHub. SDS implements a heuristic algorithm for quickly finding the approximate set(s) of the n most dissimilar items. We benchmark SDS against a Monte Carlo method, which attempts to find the exact solution through repeated random sampling. We show that for SDS to find the set of n most dissimilar conformers, our method is not only orders of magnitude faster, but is also more accurate than running the Monte Carlo for 1,000,000 iterations, each searching for set sizes n=3-7 out of a population of 50,000. We also benchmark SDS against the exact solution for example small populations, showing SDS produces a solution close to the exact solution in these instances. △ Less

Submitted 6 May, 2021; originally announced May 2021.

Program Analysis (an Appetizer)

Authors: Flemming Nielson, Hanne Riis Nielson

Abstract: This book is an introduction to program analysis that is meant to be considerably more elementary than our advanced book Principles of Program Analysis (Springer, 2005). Rather than using flow charts as the model of programs, the book follows our introductory book Formal Methods an Appetizer (Springer, 2019) using program graphs as the model of programs. In our experience this makes the underlying… ▽ More This book is an introduction to program analysis that is meant to be considerably more elementary than our advanced book Principles of Program Analysis (Springer, 2005). Rather than using flow charts as the model of programs, the book follows our introductory book Formal Methods an Appetizer (Springer, 2019) using program graphs as the model of programs. In our experience this makes the underlying ideas more accessible to our computer science and computer engineering students on the master course 02242: Program Analysis at The Technical University of Denmark. Here we have gradually replaced our use of the more elementary parts of Principles of Program Analysis with material from the current book. △ Less

Submitted 18 December, 2020; originally announced December 2020.

Comments: 208 pages

Exploring the impacts of conformer selection methods on ion mobility collision cross section predictions

Authors: Felicity F. Nielson, Sean M. Colby, Dennis G. Thomas, Ryan S. Renslow, Thomas O. Metz

Abstract: The prediction of structure dependent molecular properties, such as collision cross sections as measured using ion mobility spectrometry, are crucially dependent on the selection of the correct population of molecular conformers. Here, we report an in-depth evaluation of multiple conformation selection techniques, including simple averaging, Boltzmann weighting, lowest energy selection, low energy… ▽ More The prediction of structure dependent molecular properties, such as collision cross sections as measured using ion mobility spectrometry, are crucially dependent on the selection of the correct population of molecular conformers. Here, we report an in-depth evaluation of multiple conformation selection techniques, including simple averaging, Boltzmann weighting, lowest energy selection, low energy threshold reductions, and similarity reduction. Generating 50,000 conformers each for 18 molecules, we used the In Silico Chemical Library Engine (ISiCLE) to calculate the collision cross sections for the entire dataset. First, we employed Monte Carlo simulations to understand the variability between conformer structures as generated using simulated annealing. Then we employed Monte Carlo simulations to the aforementioned conformer selection techniques applied on the simulated molecular property - the ion mobility collision cross section. Based on our analyses, we found Boltzmann weighting to be a good tradeoff between precision and theoretical accuracy. Combining multiple techniques revealed that energy thresholds and root-mean-squared deviation-based similarity reductions can save considerable computational expense while maintaining property prediction accuracy. Molecular dynamic conformer generation tools like AMBER can continue to generate new lowest energy conformers even after tens of thousands of generations, decreasing precision between runs. This reduced precision can be ameliorated and theoretical accuracy increased by running density functional theory geometry optimization on carefully selected conformers. △ Less

Submitted 14 October, 2020; originally announced October 2020.

A Theory of Available-by-Design Communicating Systems

Authors: Hugo A. López, Flemming Nielson, Hanne Riis Nielson

Abstract: Choreographic programming is a programming-language design approach that drives error-safe protocol development in distributed systems. Starting from a global specification (choreography) one can generate distributed implementations. The advantages of this top-down approach lie in the correctness-by-design principle, where implementations (endpoints) generated from a choreography behave according… ▽ More Choreographic programming is a programming-language design approach that drives error-safe protocol development in distributed systems. Starting from a global specification (choreography) one can generate distributed implementations. The advantages of this top-down approach lie in the correctness-by-design principle, where implementations (endpoints) generated from a choreography behave according to the strict control flow described in the choreography, and do not deadlock. Motivated by challenging scenarios in Cyber-Physical Systems (CPS), we study how choreographic programming can cater for dynamic infrastructures where not all endpoints are always available. We introduce the Global Quality Calculus ($GC_q$), a variant of choreographic programming for the description of communication systems where some of the components involved in a communication might fail. GCq features novel operators for multiparty, partial and collective communications. This paper studies the nature of failure-aware communication: First, we introduce $GC_q$ syntax, semantics and examples of its use. The interplay between failures and collective communications in a choreography can lead to choreographies that cannot progress due to absence of resources. In our second contribution, we provide a type system that ensures that choreographies can be realized despite changing availability conditions. A specification in $GC_q$ guides the implementation of distributed endpoints when paired with global (session) types. Our third contribution provides an endpoint-projection based methodology for the generation of failure-aware distributed processes. We show the correctness of the projection, and that well-typed choreographies with availability considerations enjoy progress. △ Less

Submitted 17 November, 2016; originally announced November 2016.

Comments: Extended version of paper entitled "Enforcing Availability in Failure-Aware Communicating Systems", presented at FORTE 2016. 30 pages (original paper) + 19 pages of appendixes

MSC Class: 68Q55; 68Q60; 68Q85 ACM Class: D.2.4; D.3.1; D.3.2; B.8.1

A Coordination Language for Databases

Authors: Ximeng Li, Xi Wu, Alberto Lluch Lafuente, Flemming Nielson, Hanne Riis Nielson

Abstract: We present a coordination language for the modeling of distributed database applications. The language, baptized Klaim-DB, borrows the concepts of localities and nets of the coordination language Klaim but re-incarnates the tuple spaces of Klaim as databases. It provides high-level abstractions and primitives for the access and manipulation of structured data, with integrity and atomicity consider… ▽ More We present a coordination language for the modeling of distributed database applications. The language, baptized Klaim-DB, borrows the concepts of localities and nets of the coordination language Klaim but re-incarnates the tuple spaces of Klaim as databases. It provides high-level abstractions and primitives for the access and manipulation of structured data, with integrity and atomicity considerations. We present the formal semantics of Klaim-DB and develop a type system that avoids potential runtime errors such as certain evaluation errors and mismatches of data format in tables, which are monitored in the semantics. The use of the language is illustrated in a scenario where the sales from different branches of a chain of department stores are aggregated from their local databases. Raising the abstraction level and encapsulating integrity checks in the language primitives have benefited the modeling task considerably. △ Less

Submitted 16 March, 2017; v1 submitted 7 October, 2016; originally announced October 2016.

ACM Class: D.3.2

Journal ref: Logical Methods in Computer Science, Volume 13, Issue 1 (March 17, 2017) lmcs:3205

Discovering, quantifying, and displaying attacks

Authors: Roberto Vigo, Flemming Nielson, Hanne Riis Nielson

Abstract: In the design of software and cyber-physical systems, security is often perceived as a qualitative need, but can only be attained quantitatively. Especially when distributed components are involved, it is hard to predict and confront all possible attacks. A main challenge in the development of complex systems is therefore to discover attacks, quantify them to comprehend their likelihood, and commu… ▽ More In the design of software and cyber-physical systems, security is often perceived as a qualitative need, but can only be attained quantitatively. Especially when distributed components are involved, it is hard to predict and confront all possible attacks. A main challenge in the development of complex systems is therefore to discover attacks, quantify them to comprehend their likelihood, and communicate them to non-experts for facilitating the decision process. To address this three-sided challenge we propose a protection analysis over the Quality Calculus that (i) computes all the sets of data required by an attacker to reach a given location in a system, (ii) determines the cheapest set of such attacks for a given notion of cost, and (iii) derives an attack tree that displays the attacks graphically. The protection analysis is first developed in a qualitative setting, and then extended to quantitative settings following an approach applicable to a great many contexts. The quantitative formulation is implemented as an optimisation problem encoded into Satisfiability Modulo Theories, allowing us to deal with complex cost structures. The usefulness of the framework is demonstrated on a national-scale authentication system, studied through a Java implementation of the framework. △ Less

Submitted 19 October, 2016; v1 submitted 26 July, 2016; originally announced July 2016.

Comments: LMCS SPECIAL ISSUE FORTE 2014

MSC Class: 68Q60

Journal ref: Logical Methods in Computer Science, Volume 12, Issue 4 (April 27, 2017) lmcs:2178

A Framework for Hybrid Systems with Denial-of-Service Security Attack

Authors: Shuling Wang, Flemming Nielson, Hanne Riis Nielson

Abstract: Hybrid systems are integrations of discrete computation and continuous physical evolution. The physical components of such systems introduce safety requirements, the achievement of which asks for the correct monitoring and control from the discrete controllers. However, due to denial-of-service security attack, the expected information from the controllers is not received and as a consequence the… ▽ More Hybrid systems are integrations of discrete computation and continuous physical evolution. The physical components of such systems introduce safety requirements, the achievement of which asks for the correct monitoring and control from the discrete controllers. However, due to denial-of-service security attack, the expected information from the controllers is not received and as a consequence the physical systems may fail to behave as expected. This paper proposes a formal framework for expressing denial-of-service security attack in hybrid systems. As a virtue, a physical system is able to plan for reasonable behavior in case the ideal control fails due to unreliable communication, in such a way that the safety of the system upon denial-of-service is still guaranteed. In the context of the modeling language, we develop an inference system for verifying safety of hybrid systems, without putting any assumptions on how the environments behave. Based on the inference system, we implement an interactive theorem prover and have applied it to check an example taken from train control system. △ Less

Submitted 27 March, 2014; v1 submitted 24 March, 2014; originally announced March 2014.

Comments: 19 pages, 1 figures, the short version was accepted by FORTE 2014

Pushdown Systems for Monotone Frameworks

Authors: Michal Terepeta, Hanne Riis Nielson, Flemming Nielson

Abstract: Monotone frameworks is one of the most successful frameworks for intraprocedural data flow analysis extending the traditional class of bitvector frameworks (like live variables and available expressions). Weighted pushdown systems is similarly one of the most general frameworks for interprocedural analysis of programs. However, it makes use of idempotent semirings to represent the sets of properti… ▽ More Monotone frameworks is one of the most successful frameworks for intraprocedural data flow analysis extending the traditional class of bitvector frameworks (like live variables and available expressions). Weighted pushdown systems is similarly one of the most general frameworks for interprocedural analysis of programs. However, it makes use of idempotent semirings to represent the sets of properties and unfortunately they do not admit analyses whose transfer functions are not strict (e.g., classical bitvector frameworks). This motivates the development of algorithms for backward and forward reachability of pushdown systems using sets of properties forming so-called flow algebras that weaken some of the assumptions of idempotent semirings. In particular they do admit the bitvector frameworks, monotone frameworks, as well as idempotent semirings. We show that the algorithms are sound under mild assumptions on the flow algebras, mainly that the set of properties constitutes a join semi-lattice, and complete provided that the transfer functions are suitably distributive (but not necessarily strict). △ Less

Submitted 17 July, 2013; originally announced July 2013.

Design-Efficiency in Security

Authors: Ender Yüksel, Hanne Riis Nielson, Flemming Nielson

Abstract: In this document, we present our applied results on balancing security and performance using a running example, which is based on sensor networks. These results are forming a basis for a new approach to balance security and performance, and therefore provide design-efficiency of key updates. We employ probabilistic model checking approach and present our modelling and analysis study using PRISM… ▽ More In this document, we present our applied results on balancing security and performance using a running example, which is based on sensor networks. These results are forming a basis for a new approach to balance security and performance, and therefore provide design-efficiency of key updates. We employ probabilistic model checking approach and present our modelling and analysis study using PRISM model checker. △ Less

Submitted 5 February, 2013; originally announced February 2013.

Report number: IMM--TECHNICALREPORT?2013-03

Roadmap Document on Stochastic Analysis

Authors: Bo Friis Nielsen, Flemming Nielson, Henrik Pilegaard, Michael James Andrew Smith, Ender Yüksel, Kebin Zeng, Lijun Zhang

Abstract: This document was prepared as part of the MT-LAB research centre. The research centre studies the Modelling of Information Technology and is a VKR Centre of Excellence funded for five years by the VILLUM Foundation. You can read more about MT-LAB at its webpage www.MT-LAB.dk. The goal of the document is to serve as an introduction to new PhD students addressing the research goals of MT-LAB. As s… ▽ More This document was prepared as part of the MT-LAB research centre. The research centre studies the Modelling of Information Technology and is a VKR Centre of Excellence funded for five years by the VILLUM Foundation. You can read more about MT-LAB at its webpage www.MT-LAB.dk. The goal of the document is to serve as an introduction to new PhD students addressing the research goals of MT-LAB. As such it aims to provide an overview of a number of selected approaches to the modelling of stochastic systems. It should be readable not only by computers scientists with a background in formal methods but also by PhD students in stochastics that are interested in understanding the computer science approach to stochastic model checking. We have no intention of being encyclopedic in our treatment of the approaches or the literature. Rather we have made the selection of material based on the competences of the groups involved in or closely affiliated to MT-LAB, so as to ease the task of the PhD students in navigating an otherwise vast amount of literature. We have decided to publish the document in case other young researchers may find it helpful. The list of authors reflect those that have at times played a significant role in the production of the document. △ Less

Submitted 27 September, 2012; originally announced September 2012.

Comments: This work has been supported by MT-LAB, a VKR Centre of Excellence for the Modelling of Information Technology

Lattice based Least Fixed Point Logic

Authors: Piotr Filipiuk, Flemming Nielson, Hanne Riis Nielson

Abstract: As software systems become more complex, there is an increasing need for new static analyses. Thanks to the declarative style, logic programming is an attractive formalism for specifying them. However, prior work on using logic programming for static analysis focused on analyses defined over some powerset domain, which is quite limiting. In this paper we present a logic that lifts this restriction… ▽ More As software systems become more complex, there is an increasing need for new static analyses. Thanks to the declarative style, logic programming is an attractive formalism for specifying them. However, prior work on using logic programming for static analysis focused on analyses defined over some powerset domain, which is quite limiting. In this paper we present a logic that lifts this restriction, called Lattice based Least Fixed Point Logic (LLFP), that allows interpretations over any complete lattice satisfying Ascending Chain Condition. The main theoretical contribution is a Moore Family result that guarantees that there always is a unique least solution for a given problem. Another contribution is the development of solving algorithm that computes the least model of LLFP formulae guaranteed by the Moore Family result. △ Less

Submitted 23 July, 2012; originally announced July 2012.

XACML 3.0 in Answer Set Programming

Authors: Carroline Dewi Puspa Kencana Ramli, Hanne Riis Nielson, Flemming Nielson

Abstract: We present a systematic technique for transforming XACML 3.0 policies in Answer Set Programming (ASP). We show that the resulting logic program has a unique answer set that directly corresponds to our formalisation of the standard semantics of XACML 3.0 from Ramli et. al. We demonstrate how our results make it possible to use off-the-shelf ASP solvers to formally verify properties of access contro… ▽ More We present a systematic technique for transforming XACML 3.0 policies in Answer Set Programming (ASP). We show that the resulting logic program has a unique answer set that directly corresponds to our formalisation of the standard semantics of XACML 3.0 from Ramli et. al. We demonstrate how our results make it possible to use off-the-shelf ASP solvers to formally verify properties of access control policies represented in XACML, such as checking the completeness of a set of access control policies and verifying policy properties. △ Less

Submitted 18 February, 2013; v1 submitted 22 June, 2012; originally announced June 2012.

Optimizing ZigBee Security using Stochastic Model Checking

Authors: Ender Yüksel, Hanne Riis Nielson, Flemming Nielson, Matthias Fruth, Marta Kwiatkowska

Abstract: ZigBee is a fairly new but promising wireless sensor network standard that offers the advantages of simple and low resource communication. Nevertheless, security is of great concern to ZigBee, and enhancements are prescribed in the latest ZigBee specication: ZigBee-2007. In this technical report, we identify an important gap in the specification on key updates, and present a methodology for determ… ▽ More ZigBee is a fairly new but promising wireless sensor network standard that offers the advantages of simple and low resource communication. Nevertheless, security is of great concern to ZigBee, and enhancements are prescribed in the latest ZigBee specication: ZigBee-2007. In this technical report, we identify an important gap in the specification on key updates, and present a methodology for determining optimal key update policies and security parameters. We exploit the stochastic model checking approach using the probabilistic model checker PRISM, and assess the security needs for realistic application scenarios. △ Less

Submitted 30 May, 2012; originally announced May 2012.

Modelling Chinese Smart Grid: A Stochastic Model Checking Case Study

Authors: Ender Yüksel, Hanne Riis Nielson, Flemming Nielson, Huibiao Zhu, Heqing Huang

Abstract: Cyber-physical systems integrate information and communication technology functions to the physical elements of a system for monitoring and controlling purposes. The conversion of traditional power grid into a smart grid, a fundamental example of a cyber-physical system, raises a number of issues that require novel methods and applications. In this context, an important issue is the verification o… ▽ More Cyber-physical systems integrate information and communication technology functions to the physical elements of a system for monitoring and controlling purposes. The conversion of traditional power grid into a smart grid, a fundamental example of a cyber-physical system, raises a number of issues that require novel methods and applications. In this context, an important issue is the verification of certain quantitative properties of the system. In this technical report, we consider a specific Chinese Smart Grid implementation and try to address the verification problem for certain quantitative properties including performance and battery consumption. We employ stochastic model checking approach and present our modelling and analysis study using PRISM model checker. △ Less

Submitted 30 May, 2012; originally announced May 2012.

Layered Fixed Point Logic

Authors: Piotr Filipiuk, Flemming Nielson, Hanne Riis Nielson

Abstract: We present a logic for the specification of static analysis problems that goes beyond the logics traditionally used. Its most prominent feature is the direct support for both inductive computations of behaviors as well as co-inductive specifications of properties. Two main theoretical contributions are a Moore Family result and a parametrized worst case time complexity result. We show that the log… ▽ More We present a logic for the specification of static analysis problems that goes beyond the logics traditionally used. Its most prominent feature is the direct support for both inductive computations of behaviors as well as co-inductive specifications of properties. Two main theoretical contributions are a Moore Family result and a parametrized worst case time complexity result. We show that the logic and the associated solver can be used for rapid prototy** and illustrate a wide variety of applications within Static Analysis, Constraint Satisfaction Problems and Model Checking. In all cases the complexity result specializes to the worst case time complexity of the classical methods. △ Less

Submitted 12 April, 2012; originally announced April 2012.

Secondary use of data in EHR systems

Authors: Fan Yang, Chris Hankin, Flemming Nielson, Hanne Riis Nielson

Abstract: We show how to use aspect-oriented programming to separate security and trust issues from the logical design of mobile, distributed systems. The main challenge is how to enforce various types of security policies, in particular predictive access control policies - policies based on the future behavior of a program. A novel feature of our approach is that advice is able to analyze the future use of… ▽ More We show how to use aspect-oriented programming to separate security and trust issues from the logical design of mobile, distributed systems. The main challenge is how to enforce various types of security policies, in particular predictive access control policies - policies based on the future behavior of a program. A novel feature of our approach is that advice is able to analyze the future use of data. We consider a number of different security policies, concerning both primary and secondary use of data, some of which can only be enforced by analysis of process continuations. △ Less

Submitted 20 January, 2012; originally announced January 2012.

Comments: 40 pages

The Logic of XACML - Extended

Authors: Carroline Dewi Puspa Kencana Ramli, Hanne Riis Nielson, Flemming Nielson

Abstract: We study the international standard XACML 3.0 for describing security access control policy in a compositional way. Our main contribution is to derive a logic that precisely captures the idea behind the standard and to formally define the semantics of the policy combining algorithms of XACML. To guard against modelling artefacts we provide an alternative way of characterizing the policy combining… ▽ More We study the international standard XACML 3.0 for describing security access control policy in a compositional way. Our main contribution is to derive a logic that precisely captures the idea behind the standard and to formally define the semantics of the policy combining algorithms of XACML. To guard against modelling artefacts we provide an alternative way of characterizing the policy combining algorithms and we formally prove the equivalence of these approaches. This allows us to pinpoint the shortcoming of previous approaches to formalization based either on Belnap logic or on D-algebra. △ Less

Submitted 17 October, 2011; originally announced October 2011.

Comments: Extended paper from The Logic of XACML, presented in FACS 2011 (8th International Symposium on Formal Aspects of Component Software)

A Stochastic Broadcast Pi-Calculus

Authors: Lei Song, Flemming Nielson, Bo Friis Nielsen

Abstract: In this paper we propose a stochastic broadcast PI-calculus which can be used to model server-client based systems where synchronization is always governed by only one participant. Therefore, there is no need to determine the joint synchronization rates. We also take immediate transitions into account which is useful to model behaviors with no impact on the temporal properties of a system. Since i… ▽ More In this paper we propose a stochastic broadcast PI-calculus which can be used to model server-client based systems where synchronization is always governed by only one participant. Therefore, there is no need to determine the joint synchronization rates. We also take immediate transitions into account which is useful to model behaviors with no impact on the temporal properties of a system. Since immediate transitions may introduce non-determinism, we will show how these non-determinism can be resolved, and as result a valid CTMC will be obtained finally. Also some practical examples are given to show the application of this calculus. △ Less

Submitted 6 July, 2011; originally announced July 2011.

Comments: In Proceedings QAPL 2011, arXiv:1107.0746

Journal ref: EPTCS 57, 2011, pp. 74-88

Bisimulations Meet PCTL Equivalences for Probabilistic Automata

Authors: Lei Song, Lijun Zhang, Jens Chr. Godskesen, Flemming Nielson

Abstract: Probabilistic automata (PAs) have been successfully applied in formal verification of concurrent and stochastic systems. Efficient model checking algorithms have been studied, where the most often used logics for expressing properties are based on probabilistic computation tree logic (PCTL) and its extension PCTL^*. Various behavioral equivalences are proposed, as a powerful tool for abstraction… ▽ More Probabilistic automata (PAs) have been successfully applied in formal verification of concurrent and stochastic systems. Efficient model checking algorithms have been studied, where the most often used logics for expressing properties are based on probabilistic computation tree logic (PCTL) and its extension PCTL^*. Various behavioral equivalences are proposed, as a powerful tool for abstraction and compositional minimization for PAs. Unfortunately, the equivalences are well-known to be sound, but not complete with respect to the logical equivalences induced by PCTL or PCTL*. The desire of a both sound and complete behavioral equivalence has been pointed out by Segala in 1995, but remains open throughout the years. In this paper we introduce novel notions of strong bisimulation relations, which characterize PCTL and PCTL* exactly. We extend weak bisimulations that characterize PCTL and PCTL* without next operator, respectively. Further, we also extend the framework to simulation preorders. Thus, our paper bridges the gap between logical and behavioral equivalences and preorders in this setting. △ Less

Submitted 21 June, 2013; v1 submitted 10 June, 2011; originally announced June 2011.

Comments: Long version of CONCUR'11 with the same title: added extension to simulations, countable states

Journal ref: Logical Methods in Computer Science, Volume 9, Issue 2 (June 21, 2013) lmcs:1238

Efficient CSL Model Checking Using Stratification

Authors: Lijun Zhang, David N. Jansen, Flemming Nielson, Holger Hermanns

Abstract: For continuous-time Markov chains, the model-checking problem with respect to continuous-time stochastic logic (CSL) has been introduced and shown to be decidable by Aziz, Sanwal, Singhal and Brayton in 1996. Their proof can be turned into an approximation algorithm with worse than exponential complexity. In 2000, Baier, Haverkort, Hermanns and Katoen presented an efficient polynomial-time approx… ▽ More For continuous-time Markov chains, the model-checking problem with respect to continuous-time stochastic logic (CSL) has been introduced and shown to be decidable by Aziz, Sanwal, Singhal and Brayton in 1996. Their proof can be turned into an approximation algorithm with worse than exponential complexity. In 2000, Baier, Haverkort, Hermanns and Katoen presented an efficient polynomial-time approximation algorithm for the sublogic in which only binary until is allowed. In this paper, we propose such an efficient polynomial-time approximation algorithm for full CSL. The key to our method is the notion of stratified CTMCs with respect to the CSL property to be checked. On a stratified CTMC, the probability to satisfy a CSL path formula can be approximated by a transient analysis in polynomial time (using uniformization). We present a measure-preserving, linear-time and -space transformation of any CTMC into an equivalent, stratified one. This makes the present work the centerpiece of a broadly applicable full CSL model checker. Recently, the decision algorithm by Aziz et al. was shown to work only for stratified CTMCs. As an additional contribution, our measure-preserving transformation can be used to ensure the decidability for general CTMCs. △ Less

Submitted 27 June, 2012; v1 submitted 26 April, 2011; originally announced April 2011.

Comments: 18 pages, preprint for LMCS. An extended abstract appeared in ICALP 2011

ACM Class: G.3, F.4.1, F.3.1

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 2 (July 31, 2012) lmcs:1085

History-sensitive versus future-sensitive approaches to security in distributed systems

Authors: Alejandro Mario Hernandez, Flemming Nielson

Abstract: We consider the use of aspect-oriented techniques as a flexible way to deal with security policies in distributed systems. Recent work suggests to use aspects for analysing the future behaviour of programs and to make access control decisions based on this; this gives the flavour of dealing with information flow rather than mere access control. We show in this paper that it is beneficial to aug… ▽ More We consider the use of aspect-oriented techniques as a flexible way to deal with security policies in distributed systems. Recent work suggests to use aspects for analysing the future behaviour of programs and to make access control decisions based on this; this gives the flavour of dealing with information flow rather than mere access control. We show in this paper that it is beneficial to augment this approach with history-based components as is the traditional approach in reference monitor-based approaches to mandatory access control. Our developments are performed in an aspect-oriented coordination language aiming to describe the Bell-LaPadula policy as elegantly as possible. Furthermore, the resulting language has the capability of combining both history- and future-sensitive policies, providing even more flexibility and power. △ Less

Submitted 27 October, 2010; originally announced October 2010.

Comments: In Proceedings ICE 2010, arXiv:1010.5308

Journal ref: EPTCS 38, 2010, pp. 29-43