29 citations · 40 across the 13 of their papers we have counts for
13 papers
DisQ: A Model of Distributed Quantum Processors (Extended Version)
Le Chang, Saitej Yavvari, Rance Cleaveland +3
The next generation of distributed quantum processors combines single-location quantum computing and quantum networking techniques to permit large entangled qubit groups to be esta…
The Quantum Abstract Machine
Liyi Li, Le Chang, Rance Cleaveland +2
This paper develops a model of quantum behavior that is intended to support the abstract yet accurate design and functional verification of quantum communication protocols. The wor…
Expressiveness Results for Timed Modal Mu-Calculi
Rance Cleaveland, Jeroen J. A. Keiren, Peter Fontana
This paper establishes relative expressiveness results for several modal mu-calculi interpreted over timed automata. These mu-calculi combine modalities for expressing passage of (…
Resilience to Denial-of-Service and Integrity Attacks: A Structured Systems Approach
Bhaskar Ramasubramanian, M. A. Rajan, M. Girish Chandra +2
The resilience of cyberphysical systems to denial-of-service (DoS) and integrity attacks is studied in this paper. The cyberphysical system is modeled as a linear structured system…
Temporal-Logic Query Checking over Finite Data Streams
Samuel Huang, Rance Cleaveland
This paper describes a technique for inferring temporal-logic properties for sets of finite data streams. Such data streams arise in many domains, including server logs, program te…
Timed Automata Benchmark Description
Peter Fontana, Rance Cleaveland
This report contains the descriptions of the timed automata (models) and the properties (specifications) that are used as the "benchmark examples in Data structure choices for on-t…
Better Automata through Process Algebra
Rance Cleaveland
This paper shows how the use of Structural Operational Semantics (SOS) in the style popularized by the process-algebra community can lead to a more succinct and useful construction…
A Tableau Construction for Finite Linear-Time Temporal Logic
Samuel Huang, Rance Cleaveland
This paper describes a method for converting formulas in finite propositional linear-time temporal logic (Finite LTL) into finite-state automata whose languages are the models of t…
Notions of Centralized and Decentralized Opacity in Linear Systems
Bhaskar Ramasubramanian, Rance Cleaveland, Steven I. Marcus
We formulate notions of opacity for cyberphysical systems modeled as discrete-time linear time-invariant systems. A set of secret states is -ISO with respect to a set of nonsecr…
Bisimulation and Hennessy-Milner Logic for Generalized Synchronization Trees
James Ferlez, Rance Cleaveland, Steve Marcus
In this work, we develop a generalization of Hennessy-Milner Logic (HML) for Generalized Synchronization Trees (GSTs) that we call Generalized Hennessy Milner Logic (GHML). Importa…
An extensible formal semantics for UML activity diagrams
Zamira Daw, Rance Cleaveland
This paper presents an operational semantics for UML activity diagrams. The purpose of this semantics is three-fold: to give a robust basis for verifying model correctness; to help…
Corrections to A Menagerie of Timed Automata
Jeroen J. A. Keiren, Peter Fontana, Rance Cleaveland
This note corrects a technical error in the ACM Computing Surveys paper mentioned in the title. The flaw involved constructions for showing that timed automata with urgent location…
The Power of Proofs: New Algorithms for Timed Automata Model Checking (with Appendix)
Peter Fontana, Rance Cleaveland
This paper presents the first model-checking algorithm for an expressive modal mu-calculus over timed automata, , and reports performance resul…