A5048229897- Formal Methods in Verification
- Logic, programming, and type systems
- Logic, Reasoning, and Knowledge
- Petri Nets in System Modeling
- Distributed systems and fault tolerance
- Business Process Modeling and Analysis
- Advanced Software Engineering Methodologies
- Service-Oriented Architecture and Web Services
- semigroups and automata theory
- Mobile Ad Hoc Networks
- Software Testing and Debugging Techniques
- Model-Driven Software Engineering Techniques
- Security and Verification in Computing
- Wireless Networks and Protocols
- Advanced Algebra and Logic
- Adversarial Robustness in Machine Learning
- Safety Systems Engineering in Autonomy
- Access Control and Trust
- Vehicular Ad Hoc Networks (VANETs)
- Software Reliability and Analysis Research
- Simulation Techniques and Applications
- Computability, Logic, AI Algorithms
- Software Engineering Research
- Semantic Web and Ontologies
- Blockchain Technology Applications and Security
UNSW Sydney
2015-2024
University of Edinburgh
2004-2024
Data61
2013-2023
Commonwealth Scientific and Industrial Research Organisation
2016-2023
Australian National University
2020-2023
Eindhoven University of Technology
2023
Stanford University
1995-2021
Peking University
2018
École Polytechnique
2017
Technische Universität Dresden
2015
Reactive, generative, and stratified models are considered within the framework of PCCS, a specification language for probabilistic processes. A structural operational semantics given as set inference rules each models, notion bisimulation semantics, some conference proofs presented.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">></ETX>
We consider the relational characterisation of branching bisimilarity with explicit divergence. prove that it is an equivalence and coincides original definition divergence in terms colou
This paper proposes a notion of branching bisimilarity for non-deterministic probabilistic processes. In order to characterize the corresponding rooted bisimilarity, an equational theory is proposed basic, recursion-free process language with as well choice. The proof completeness axiomatization builds on strong one hand and concrete process, i.e. that does not display (partially) inert $\tau$-moves, other hand. approach first presented fragment calculus next generalized incorporate choice, too.
We propose AWN (Algebra for Wireless Networks), a process algebra tailored to the modelling of Mobile Ad hoc Network (MANET) and Mesh (WMN) protocols. It combines novel treatments local broadcast, conditional unicast data structures. In this framework we present rigorous analysis On-Demand Distance Vector (AODV) protocol, popular routing protocol designed MANETs WMNs, one four protocols currently standardised by IETF MANET working group. give complete unambiguous specification thereby...
This paper proposes a definition of what it means for one system description language to encode another one, thereby enabling an ordering languages with respect expressive power. I compare the proposed other definitions encoding and expressiveness found in literature, illustrate on case study: comparing power CCS CSP.
In 1992 Wang & Larsen extended the may- and must preorders of De Nicola Hennessy to processes featuring probabilistic as well nondeterministic choice. They concluded with two problems that have remained open throughout years, namely find complete axiomatisations alternative characterisations for these preorders. This paper solves both finite silent moves. It characterises may preorder in terms simulation, failure simulation. also gives a characterisation using modal logic. Finally it...
We develop a general testing scenario for probabilistic processes, giving rise to two theories: may and must testing. These are applied simple version of the process calculus CSP. examine algebraic theory testing, show that many axioms standard no longer valid in our setting; even non-probabilistic CSP distinguishing power tests is much greater than tests. method deriving inequations based on extension notion simulation. Using this, we obtain complete axiomatisation processes subject
We study the equivalence relation on states of labelled transition systems satisfying same formulas in Computation Tree Logic without next state modality (CTL-X). This is obtained by De Nicola & Vaandrager translating to Kripke structures, while lifting totality restriction latter. They characterised it as divergence sensitive branching bisimulation equivalence. find that this fails be a congruence for interleaving parallel composition. The reason proposed application CTL-X non-total...
A cornerstone of the theory proof nets for unit-freemultiplicative linear logic (MLL) is abstract representation cut-freeproofs modulo inessential commutations rules. The only knownextension to additives, based on monomial weights, fails topreserve this key feature: a host cut-free cancorrespond same proof. Thus problem offinding satisfactory notion net unit-freemultiplicative-additive (MALL) has remained open since theincep-tion in 1986. We present new definition MALLproof which remains...