Macquarie University, Sydney Macquarie University ResearchOnline

Showing items 1 - 15 of 19.

Add to Quick Collection   All 19 Results

Sort:
 Add All Items to Quick Collection
Date: 2013
Language: eng
Resource Type: conference paper
Identifier: http://hdl.handle.net/1959.14/281038
Description: We give a new true-concurrent model for probabilistic concurrent Kleene algebra. The model is based on probabilistic event structures, which combines ideas from Katoen's work on probabilistic concurre ... More
Reviewed: Reviewed
Date: 2013
Language: eng
Resource Type: conference paper
Identifier: http://hdl.handle.net/1959.14/262839
Description: We provide an extension of concurrent Kleene algebras to account for probabilistic properties. The algebra yields a unified framework containing nondeterminism, concurrency and probability and is soun ... More
Reviewed: Reviewed
Date: 2012
Language: eng
Resource Type: conference paper
Identifier: http://hdl.handle.net/1959.14/190328
Description: We propose a novel domain-theoretic model for nondeterminism, probability and hidden state, with relations on it that compare information flow. One relation is Smyth-like, based on a structural, refin ... More
Reviewed: Reviewed
Date: 2012
Language: eng
Resource Type: conference paper
Identifier: http://hdl.handle.net/1959.14/172380
Description: We propose a process algebra for wireless mesh networks that combines novel treatments of local broadcast, conditional unicast and data structures. In this framework, we model the Ad-hoc On-Demand Dis ... More
Reviewed: Reviewed
Date: 2012
Language: eng
Resource Type: conference paper
Identifier: http://hdl.handle.net/1959.14/172368
Description: This paper describes an automated, formal and rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol, a popular protocol used in wireless mesh networks. We give a brief over ... More
Reviewed: Reviewed
Date: 2011
Language: eng
Resource Type: conference paper
Identifier: http://hdl.handle.net/1959.14/158895
Description: The role played by counterexamples in standard system analysis is well known; but less common is a notion of counterexample in probabilistic systems refinement. In this paper we extend previous work u ... More
Reviewed: Reviewed
Date: 2011
Language: eng
Resource Type: conference paper
Identifier: http://hdl.handle.net/1959.14/150146
Description: We show that a class of automata modulo simulation equivalence forms a model of probabilistic Kleene algebra. We prove completeness of this model with respect to continuous probabilistic Kleene algebr ... More
Reviewed: Reviewed
Date: 2011
Language: eng
Resource Type: conference paper
Identifier: http://hdl.handle.net/1959.14/150141
Description: We use well-known algebraic concepts like semirings and matrices to model and argue about Wireless Mesh Networks. These networks are used in a wide range of application areas, including public safety ... More
Reviewed: Reviewed
Date: 2010
Language: eng
Resource Type: conference paper
Identifier: http://hdl.handle.net/1959.14/148088
Description: We give a quantitative sequential model for noninterference security with probability (but not demonic choice), and a novel refinement order that we prove to be the greatest compositional relation con ... More
Reviewed: Reviewed
Date: 2009
Language: eng
Resource Type: conference paper
Identifier: http://hdl.handle.net/1959.14/148619
Description: Security and probability are both artefacts that we hope to bring increasingly within the reach of refinement-based Formal Methods; although we have worked on them separately, in the past, the goal ha ... More
Reviewed: Reviewed
Date: 2007
Language: eng
Resource Type: journal article
Identifier: http://hdl.handle.net/1959.14/25042
Description: The μ-calculus is a powerful tool for specifying and verifying transition systems, including those with both demonic (universal) and angelic (existential) choice; its quantitative generalization qMμ e ... More
Reviewed: Reviewed
Date: 2006
Language: eng
Resource Type: journal article
Identifier: http://hdl.handle.net/1959.14/9656
Description: The quantitative μ-calculus qMμ extends the applicability of Kozen's standard μ-calculus [D. Kozen, Results on the propositional μ-calculus, Theoretical Computer Science 27 (1983) 333–354] to probabil ... More
Reviewed: Reviewed
Date: 2006
Language: eng
Resource Type: book chapter
Identifier: http://hdl.handle.net/1959.14/10711
Description: As explained in Chapter 1, Dijkstra’s guarded-command language, which we call <i>GCL</i>, was introduced as an intellectual framework for rigorous reasoning about imperative sequential programs; one o ... More
Date: 2005
Language: eng
Resource Type: book
Identifier: http://hdl.handle.net/1959.14/6448
Description: The book is a focused survey on probabilistic program semantics, conceived to tell a coherent story with a uniform notation. It is grouped into three themes: Part I is for 'users' of the techniques wh ... More
Date: 2005
Language: eng
Resource Type: journal article
Identifier: http://hdl.handle.net/1959.14/146586
Description: Herman's Ring [Inform. Process. Lett. 35 (1990) 63; http://www.cs.uiowa.edu/ftp/selfstab/H90.ps.gz] is an algorithm for self-stabilization of N identical processors connected uni-directionally in a sy ... More
Reviewed: Reviewed