Publications

This page is not intended to be accessed directly, but rather via the list of complete references to papers or theses. Most of the time the on-line versions are technical reports and the like, which contain the same material as the published paper but differ in style. A few times several published papers are aggregated together into such an internal document. Whenever a paper is accessible for free from the publisher a link to the published version is provided instead.

Unrestricted and Disjoint Operations over Multi-Stack Visibly Pushdown Languages

by Stefan D Bruda and Md. Tawhid Bin Waez, in Proceedings of the 6th International Conference on Software and Data Technologies, July 2011, Seville, Spain. A preliminary version is available.

Sublinear Space Real-Time Turing Machines Cannot Count

by Stefan D Bruda, in Proceedings of the 8th International Conference on Information Technology: New Generations, April 2011, Las Vegas, NV. A preliminary version is available.

Model Checking Is Refinement: Computation Tree Logic Is Equivalent to Failure Trace Testing

by Stefan D. Bruda and Zhyiu Zhang. Includes the material from Refinement Is Model Checking: From Failure Trace Tests to Computation Tree Logic (SEA 2009) and from Model Checking Is Refinement: From Computation Tree Logic to Failure Trace Testing (ICSOFT 2010). An on-line version is available.

A Testing Theory for Real-Time Systems

by Chun Dai and Stefan D Bruda, Includes the material from A Testing Framework for Real-Time Specifications (SEA 2008), Timed Test Generation Based on Timed Temporal Logic (ICAI 2010) and A Testing Theory for Real-Time Systems (International Journal of Computers). An on-line version is available.

Relations Between Several Parallel Computational Models

by Stefan D. Bruda and Yuanqiao Zhang, in Scalable Computing: Practice and Experience, 10:2 (2009), pp. 163-172. The on-line version is available directly from the publisher.

Communicating Visibly pushdown Processes

by Stefan D. Bruda and Md. Tawhid Bin Waez, in Proceedings of the 17th International Conference on Control Systems and Computer Science, 26-29 May 2009, Bucharest, Romania. A preliminary version is available.

Visibly Pushdown Languages Are Closed under Prefix, Shuffle, and Hiding

by Stefan D Bruda and Md Tawhid Bin Waez, in Computational Engineering in Systems Applications: Selected Papers from the WSEAS Conferences in Heraklion, Greece, July 22-25 2008. No on-line version available yet.

Collapsing the Hierarchy of Parallel Computational Models

By Stefan D. Bruda and Yuanqiao Zhang. Includes material from The Shared Memory Hierarchy: The PRAM is as powerful as the BSR (ISPDC 2008), Why Shared Memory Matters to VLSI Design: The BSR Is as Powerful as Reconfiguration (IPDPS 2008), and Collapsing the Hierarchy of Parallel Computational Models (IJFCS). An on-line version is available. An extended version has been published under the title Reconfiguration is Shared Memory: Collapsing the Hierarchy of Parallel Models with Reconfigurable Buses and Shared Memory (LAP, January 2010).

Size Matters: Logarithmic Space Is Real Time

By Stefan D Bruda and Selim G. Akl. A preliminary version of the paper published in the International Journal of Computers and Applications is available. It also contains material from On the relation between parallel real-time computations and logarithmic space (PDCS 2002) and The characterization of parallel real-time optimization problems (16th Annual International Symposium on High Performance Computing Systems and Applications 2002).

A more preliminary version is also available; this version contains a number of flaws in the presentation of the main matter, but also supplementary material. Thus the overlapping material is better reviewed using the first document, while one should review the extra material from this second document.

The Graph Accessibility Problem and the Universality of the Collision CRCW Conflict Resolution Rule

By Stefan D. Bruda. This paper contains most of the material from The Graph Accessibility Problem and the Universality of the Collision CRCW Conflict Resolution Rule (WSEAS Transactions on Computers) and from The Characterization of Constant Time Computations and the Universality of Collision Rule on Models with Reconfigurable Buses (10th WSEAS International Conference on Computers, 2006).

RTSync

The RTSync page contains between others the material from Distributed, Real-Time Programming on Commodity POSIX Systems: A Preliminary Report (ISPDC 2006) and Distributed, Real-Time Programming Based on a Formal Semantics on Commodity POSIX Systems with no In-Kernel Real-Time Support (RRA 2008).

Preorder Relations

A slightly older version of the book chapter (by Stefan D. Bruda, in Model-Based Testing of Reactive Systems: Advanced Lectures, Springer Lecture Notes in Computer Science 3472, 2005) is available; note in particular that page numbers do not match. Includes references and index.

On limits on the computational power of data-accumulating algorithms

A slightly earlier version than the one published in Information Processing Letters (86 (2003), by Stefan D. Bruda and Selim G. Akl) is available.

Real-time computation: A formal definition and its applications

By Stefan D. Bruda and Selim G. Akl. The most complete variant is available and includes almost all the material from Towards a meaningful formal definition of real-time computations, (ISCA 15th International Conference on Computers and Their Applications, 2000), Real-Time Computation: A Formal Definition and Its Applications (IPDPS 2001), and the IJCA paper (an aggregate of the first two).

Parallel Real-Time Complexity Theory

by Stefan D. Bruda, PhD thesis, Department of Computing and Information Science, Queen's University at Kingston, April 2002.

Abstract: We present a new complexity theoretic approach to real-time computations. We define timed omega-languages as a new formal model for such computations, that we believe to allow a unified treatment of all variants of real-time computations that are meaningful in practice. To our knowledge, such a practically meaningful formal definition does not exist at this time.

In order to support our claim that timed omega-languages capture all the real-time characteristics that are important in practice, we use this formalism to model the two most important features of real-time algorithms, namely the presence of deadlines and the real-time arrival of input data. We emphasize the expressive power of our model by using it to formalize aspects from the areas of real-time database systems and ad hoc networks.

We also offer a complexity theoretic characterization of parallel real-time computations. First, we define complexity classes that capture the intuitive notion of resource requirements for real-time computations in a parallel environment. Then, we show that real-time algorithms form an infinite hierarchy with respect to the number of processors used, and that all the problems solvable in nondeterministic logarithmic space (NLOGSPACE) can be solved in real time by a parallel machine, no matter how tight the real-time constraints are. As well, we show that, once real-time constraints are dropped, several other real-time problems are in effect in NLOGSPACE. Therefore, we conjecture that NLOGSPACE contains exactly all the computations that admit feasible (poly(n) processors) real-time parallel implementations.

In the context of these results, the issue of real-time optimization problems is investigated. We identify the class of such problems that are solvable in real time, and we show that, for a large class of optimization problems, a parallel algorithm can report in real time a solution that is arbitrarily better than the solution reported by a sequential algorithm.

We also address the problem of real-time approximation algorithms. We identify problems that do not admit good approximation solutions in real time. We also show that bin packing admits a good real-time approximation algorithm.

The complete manuscript is available as PDF (930 K characters).

Pursuit and evasion on a ring: An infinite hierarchy for parallel real-time systems

By Stefan D. Bruda and Selim G. Akl. This version includes almost all the material from Parallel Real-Time Complexity: A Strong Infinite Hierarchy (SIROCCO 2001) and Pursuit and Evasion on a Ring: An Infinite Hierarchy for Parallel Real-Time Systems (Theory of Computing Systems).

On the necessity of formal models for real-time parallel computations

By Stefan D. Bruda and Selim G. Akl, in Parallel Processing Letters, 11 (2001). A preliminary version is available.

A case study in real-time parallel computation: Correcting algorithms

This document is an earlier version of the paper by Stefan D. Bruda and Selim G. Akl published in the Journal of Parallel and Distributed Computing 61 (2001).

Improving a solution's quality through parallel processing

By Selim G. Akl and Stefan D. Bruda, in Journal of Supercomputing 19 (2001). No on-line version is available.

The characterization of data-accumulating algorithms

This version is almost identical to the paper published in Theory of Computing Systems (and includes the IPDPS paper).

Parallel real-time numerical computation: Beyond speedup III

This Queen's technical report is a preliminary version of the paper in the International Journal of Computers and their Applications, 7 (2000).

Parallel real-time cryptography: Beyond speedup II

This Queen's technical report is a preliminary version of the paper in Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, Las Vegas, NV, 2000.

Parallel real-time optimization: Beyond speedup

This Queen's technical report is a preliminary version of the paper in Parallel Processing Letters, 9 (1999).

On the computational complexity of context-free parallel communicating grammar systems

By Stefan D. Bruda, this paper appeared in Springer Lecture Notes in Computer Science 1218.

MSc Theses

A Testing Framework for Real-Time Specifications

By Chun Dai, December 2008, QA 76.54 .D34 2008 (Old Library). Full paper (PDF).

This thesis proposes a new semantic model for reasoning about real-time system specifications featuring a combination of timed processes and formulas in linear-timed temporal logic with time constraints (TLTL). Based on a theory of timed omega-final states, the thesis presents a framework of timed testing and two refinement timed preorders similar to De Nicola and Hennessy's may and must testing. The paper also provides alternative characterizations for these relations to show that the new preorders are extensions of the traditional preorders and to lay the basis for a unified logical and algebraic approach to conformance testing of real-time systems. The thesis then establishes a tight connection between TLTL formula satisfaction and the timed must-preorder. More precisely, it is shown that a timed labeled transition system satisfies a TLTL formula if and only if it refines an appropriately defined timed process constructed from the formula. Consequently, we developed a timed must-preorder which allows for a uniform treatment of traditional notions of process refinement and model checking under time constraints. The implications of this novel theory are illustrated by means of a simple example system, in which some components are specified as transition systems and others as TLTL formulas. Key words: real time, real-time transition system, timed process, timed preorder, timed testing, conformance testing, model checking, LTL.

Commmmunicating Visibly pushdown Processes

By Md. Tawhid Bin Waez, December 2008, QA 76.9 .F67 B56 2008 (Old Library). Full paper (PDF).

Visibly pushdown languages are a subclass of context-free languages that is closed under all the useful operations, namely union, intersection, complementation, renaming, concatenation, prefix, and Kleene star. The existence of a concurrent, fully compositional process algebra based on such languages require that these languages be also closed under two more operations, namely shuffle, and hiding. We prove here both of these closure properties. We also give the semantics of visibly pushdown automata in terms of labelled transition systems. We then propose Communicating Visibly pushdown Processes (CVP), a fully compositional concurrent process algebra based on visibly pushdown automata. CVP is a superset of CSP, thus combining all the good properties of finite-state algebrae with context-free features. Unlike any other process algebra, CVP includes support for parallel composition but also for self-embedding recursion. We present the syntax, operational semantics, trace semantics, trace specification, and trace verification of CVP. A CVP trace observer can extract stack and module information from the trace; as a result one can specify and verify many software properties which cannot be specified in any other existing process algebra. Such properties include the access control of a module, stack limits, concurrent stack properties, internal property of a module, pre-/post-conditions of a module, etc. CVP lays the basis of algebraic conformance testing for infinite-state processes, such as application software.

Model Checking is Refining—Computational Temporal Logic is Equivalent to Failure Trace Testing

By Zhyiu Zhang, December 2008, QA 76.76 .V47 Z53 2008 (Old Library). Full paper (PDF).

The two major systems of formal verification are model checking and algebraic model-based testing. Model checking is based on some form of temporal logic such as LTL or CTL. The most powerful and realistic logic being used is CTL, which is capable of expressing most interesting properties of processes such as liveness and safety properties. Model-based testing is based on some operational semantics of processes (such as traces, failures, or both) and their associated preoders. The most fine-grained preorder beside bisimulation (of theoretical importance only) is the one based on failure traces. We show that these two most powerful variants are equivalent. That is to say, we show that for any failure trace test, there exists a CTL formula equivalent to it (meaning that a system passes the test if and only if the system satisfies the formula and the other way around). When we specify the system, we can use temporal logic formulas such as CTL formulas to express the properties of it. We can also use algebraic method such as labelled transition system or finite state automaton to describe the system's desired behaviour. If parts of a larger system are specified by these two means at the same time, combining the result of doing model checking and the result of applying model-based testing won't be ideal, satisfactory and even correct. In this case, we convert one specification to the form of the other. We then do a formal verification for the whole system. The result will be more convincing and correct

The Relationship Between Several Parallel Computational Models

By Yuanqiao Zhang, December 2008, QA 76.58 .Z53 2008 (Old Library). Full paper (PDF).

The Parallel Random Access Machine (PRAM for short) is the most convenient and widely used model of parallel computation. Other, more complex models have also been studied. Examples include the Broadcast with Selective Reduction (or BSR) and the Reconfigurable Multiple Bus Machine (or RMBM). While the PRAM and the BSR are shared memory models, the RMBM accomplishes the communication between processors using buses. In this thesis we identify surprising relationships between these models. We show that several variants are equivalent with each other in a strong sense, and we establish strict distinctions between the other variants. Some models are folklorically considered feasible and some others are not considered so. We find a delimitation that matches the folklore, but we also find important (and intriguing) equivalencies.