We study the complexity of temporal logics over concurrent systems that can be described by Mazurkiewicz traces. We develop a general method to prove that the uniform satisfiability problem of local temporal logics is in PSPACE. We also demonstrate that this method applies to all known local temporal logics.

We review the characterization of communicating finite-state machines whose behaviors have universally or existentially bounded channels. These results rely on the theory of Mazurkiewicz traces. We investigate the question whether channel bound conditions are decidable for a given communicating finite-state machine.

When system runs are modeled with interval orders, interval order structures are useful tools to model abstract concurrent histories, i.e. sets of equivalent system runs. For the general cases, Mazurkiewicz traces allow a representation of the entire partial order by a single sequence with independency relations, and Comtraces allow a representation of stratified order structures by single step sequences with appropriate simultaneity and serializability relations. Unfortunately, both of them are unable to clearly describe the abstract interval order semantics of inhibitor nets. The goal of the thesis is to provide a monoid based model called Interval Traces that would allow a single sequence of beginnings and endings to represent the entire stratified order structures as well as all equivalent interval order observations. And the thesis will also show how interval order structures can be modelled by interval traces and how interval traces can be used to describe interval order semantics. / Thesis / Doctor of Philosophy (PhD)