{'fraction_non_alphanumeric': 0.01984126984126984, 'fraction_numerical': 0.001763668430335097, 'mean_word_length': 5.099462365591398, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Model Checking and Expressiveness for First Order Process Algebras

Process algebras are coming into increasing use as specification tools for concurrent systems. Specifications are given as terms; the appropriate use of the algebra's operations lends useful structure to the specifications. As process algebraic specifications resemble programs, they appeal to programmers' intuitions. 
Since there are many different forms of concurrency, there is a correspondingly large variety of process algebras. In order to study these systems in a unified framework, a metatheory of process algebras based on structured operational semantics has been developed (dS85, Blo89) that uses constraints on the rule formats by which operations are defined to prove useful properties, e.g. that an equivalence relation on terms is also a congruence. This thesis examines applications of this metatheory. 
We first consider the problem of efficiently generalizing tools to support process algebraic methods for specification and verification. There is a variety of such tools available for specific process algebras, e.g., the tools of LOTOSphere (LOT) are intended for use with the process algebra LOTOS. Here, we develop an efficient model checker that is parameterized by a useful class of first order process algebras that is competitive with custom tools. In addition to generalizing existing model checkers for specific process algebras, this tool can be used with ad-hoc application specific ones as well. As a case study, we define an appropriate process algebra to specify the Solaris threads library. Properties of suitably abstracted threads programs may thus be verified using our model checker. 
We also investigate the expressiveness of the process algebras CCS, CSP, and ACP, in a SOS framework. We look at the rule formats that can be defined in each system, and consider the interdefinability of their operations. We suggest extensions to CCS and CSP to obtain general expressiveness up to branching bisimulation, though this is not necessary for ACP. We also use tools from the metatheory to explain why certain operations are not interdefinable in these systems. As an auxiliary result we obtain a standard form for a static subset of CCS, up to strong bisimulation.