Publication:3777424
From MaRDI portal
zbMath0637.68007MaRDI QIDQ3777424
Publication date: 1985
traceparallel processessequential processesLispinter-process communicationcombination of different devicescomprehension of formal definitionsvariety of events
Formal languages and automata (68Q45) Abstract data types; algebraic specification (68Q65) Research exposition (monographs, survey articles) pertaining to computer science (68-02) General topics in the theory of software (68N01)
Related Items
Modelling web-service uncertainty: the angel/daemon approach, A weak semantic approach to bisimulation metrics in models with nondeterminism and continuous state spaces, Algebraic specification and proof of a distributed recovery algorithm, Specification and verification of database dynamics, Probabilistic and nondeterministic aspects of anonymity, Cameo: an alternative model of concurrency for Eiffel, A shared memory algorithm and proof for the generalized alternative construct in CSP, On observability of discrete-event systems, Modular design of real-time systems using hierarchical communicating real-time state machines, Coverage metrics for temporal logic model checking, Creol: A type-safe object-oriented model for distributed concurrent systems, A calculus and logic of resources and processes, Transition systems, metric spaces and ready sets in the semantics of uniform concurrency, A basic algebra of stateless connectors, Question-guided stubborn set methods for state properties, Duplication of constants in process algebra, Preferential choice and coordination conditions, Fair testing, SOS formats and meta-theory: 20 years after, On using data abstractions for model checking refinements, Resources, concurrency, and local reasoning, Generating the syntactic and semantics graphs for a Markovian process algebra, A criterion for atomicity revisited, Compositional reasoning about active objects with shared futures, Revisiting sequential composition in process calculi, Concurrent weighted logic, Axiomatizing Lüttgen \& Vogler's ready simulation for finite processes in \(\mathrm{CLL}_{R}\), Generating symbolic traces in the insertion modeling system, Theory of interaction, Separability and the detection of hidden channels, Automated analysis of mutual exclusion algorithms using CCS, Equational reasoning about nondeterministic processes, Some behavioural aspects of net theory, An operational semantics of occam, The projection of systolic programs, Step semantics for ``true concurrency with recursion, A model of reconfiguration in communicating sequential processes, Contractions in comparing concurrency semantics, Modeling spiking neural networks, Specification of communicating processes: temporal logic versus refusals-based refinement, The neglected pillar of material computation, Model checking duration calculus: a practical approach, Adas and the equational theory of if-then-else, Automatic verification of distributed systems: the process algebra approach., Formalization of an architectural model for exception handling coordination based on CA action concepts, Algebra and logic for access control, A process algebraic framework for specification and validation of real-time systems, Pushdown module checking, Lifting non-finite axiomatizability results to extensions of process algebras, An exact correspondence between a typed pi-calculus and polarised proof-nets, Alternating states for dual nondeterminism in imperative programming, Is observational congruence on \(\mu \)-expressions axiomatisable in equational Horn logic?, Lazy behavioral subtyping, Synchronous Kleene algebra, Nondeterministic fuzzy automata, Ready simulation for concurrency: it's logical!, Machine structure oriented control code logic, On the semantics of communicating hardware processes and their translation into LOTOS for the verification of asynchronous circuits with CADP, Fully abstract models and refinements as tools to compare agents in timed coordination languages, Refinement and verification in component-based model-driven design, A general framework for architecture composability, An operational semantics for object-oriented concepts based on the class hierarchy, Towards verification of computation orchestration, A formal semantics of extended hierarchical state transition matrices using CSP\#, On integrating confidentiality and functionality in a formal method, The behavioural semantics of Event-B refinement, Derivation of concurrent programs by stepwise scheduling of Event-B models, Introducing extra operations in refinement, Relational concurrent refinement. III: Traces, partial relations and automata, Probabilistic mobile ambients, Processes with local and global liveness requirements, Revivals, stuckness and the hierarchy of CSP models, Generating priority rewrite systems for OSOS process languages, (Bi)simulations up-to characterise process semantics, Improving performance in flexible manufacturing systems, Hardness of equivalence checking for composed finite-state systems, A UTP semantics for \textsf{Circus}, Relational concurrent refinement. II: Internal operations and outputs, Refinement, conformance and inheritance, On the relationships between notions of simulation-based security, Towards systolizing compilation, P-A logic - a compositional proof system for distributed programs, Recursive process definitions with the state operator, Receptive process theory, A completed hierarchy of true concurrent equivalences, Modelling and verification of delay-insensitive circuits using CCS and the concurrency workbench, On fluidization of discrete event models: Observation and control of continuous Petri nets, Specification completion for IOCO, Approximating Markovian testing equivalence, Deadlock-freeness of hexagonal systolic arrays, Testing for refinement in \textsf{Circus}, A CSP model with flexible parallel termination semantics, An axiom system for sequence-based specification, Process algebraic modelling of attentional capture and human electrophysiology in interactive systems, Specification-oriented semantics for communicating processes, Priorities in process algebras, A complete axiomatic semantics of spawning, A formal approach to designing delay-insensitive circuits, Process algebra and constraint programming for modeling interactions in MAS, Two case studies of semantics execution in Maude: CCS and LOTOS, Refinement-oriented probability for CSP, Testing equivalence as a bisimulation equivalence, Compositional modeling and refinement for hierarchical hybrid systems, CSP-CASL -- a new integration of process algebra and algebraic specification, Algebraic-coalgebraic specification in CoCASL, Executable structural operational semantics in Maude, Security of multi-agent systems: a case study on comparison shopping, Precise specification matching for adaptive reuse in embedded systems, Non-bisimulation-based Markovian behavioral equivalences, Behavioral complexity indicators for process algebra: The NKS approach, Resources in process algebra, Distributed speculative execution for reliability and fault tolerance: an operational semantics, Using logic to solve the submodule construction problem, Operational semantics of Framed Tempura, The \$-calculus process algebra for problem solving: A paradigmatic shift in handling hard computational problems, Joshua Guttman: pioneering strand spaces, Trace semantics and algebraic laws for MCA ARMv8 architecture based on UTP, A perspective on service orchestration, Efficient symbolic computation of process expressions, Correctness proof of a database replication protocol under the perspective of the I/O automaton model, Recognizing and learning models of social exchange strategies for the regulation of social interactions in open agent societies, The ins and outs of Petri net composition, Modular verification of protocol equivalence in the presence of randomness, Monitorability for the Hennessy-Milner logic with recursion, A compositional modelling and verification framework for stochastic hybrid systems, Functional BIP: embedding connectors in functional programming languages, Automatic analysis of complex interactions in microservice systems, Translating between models of concurrency, SMT-based generation of symbolic automata, A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency, A generalised theory of interface automata, component compatibility and error, Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving, Model checking with fairness assumptions using PAT, A general overview of formal languages for individual-based modelling of ecosystems, A reduction semantics for direct-style asynchronous observables, Logical characterisations, rule formats and compositionality for input-output conformance simulation, On the axiomatisability of priority. III: Priority strikes again, Synthesis of least restrictive controllable supervisors for extended finite-state machines with variable abstraction, On the computation of counterexamples in compositional nonblocking verification, Contextual equivalence for signal flow graphs, SOS rule formats for idempotent terms and idempotent unary operators, The IITM model: a simple and expressive model for universal composability, Discrete time stochastic and deterministic Petri box calculus dtsdPBC, A specification structure for deadlock-freedom of synchronous processes, Topology in process calculus. I: Limit behaviour of agents, Domain science and engineering from computer science to the sciences of informatics. I: Engineering, Axiomatizing weak simulation semantics over BCCSP, Parallel computation in spiking neural nets, A constraint-based language for multiparty interactions, Self-stabilizing defeat status computation: dealing with conflict management in multi-agent systems, Parallel algorithms development for programmable devices with application from cryptography, Thread algebra for strategic interleaving, A CSP model of Eiffel's SCOOP, Formalism and method, Tutorial on separation results in process calculi via leader election problems, RiskStructures: a design algebra for risk-aware machines, Denotational semantics of channel mobility in UTP-CSP, Compositional synthesis of maximally permissive supervisors using supervision equivalence, The metric linear-time branching-time spectrum on nondeterministic probabilistic processes, A process algebraic view of shared dataspace coordination, CCS with priority guards, Modelling temporal behaviour in complex systems with Timebands, Symmetric electoral systems for ambient calculi, A compositional view of derivations as interactive processes with applications to regulated and distributed rewriting, Process algebra with strategic interleaving, Complete proof systems for weighted modal logic, Simulating Turing machines on Maurer machines, Integrating a formal method into a software engineering process with UML and Java, Preservation of probabilistic information flow under refinement, Partition consistency. A case study in modeling systems with weak memory consistency and proving correctness of their implementations, The weakest specifunction, Unifying simulatability definitions in cryptographic systems under different timing assumptions, Unifying theories of reactive design contracts, An axiomatization for quantum processes to unifying quantum and classical computing, Probabilistic process algebra to unifying quantum and classical computing in closed systems, Entanglement in quantum process algebra, Formal verification for KMB09 protocol, Ensuring liveness properties of distributed systems: open problems, Model transformations across views, Safe abstractions of data encodings in formal security protocol models, A wide-spectrum language for verification of programs on weak memory models, A process calculus BigrTiMo of mobile systems and its formal semantics, Matching logic explained, A calculus of branching processes, On primitives for compensation handling as adaptable processes, Automated verification of reactive and concurrent programs by calculation, Alternative representations of P systems solutions to the graph colouring problem, \textit{D\_PSNI}: delimited persistent stochastic non-interference, Bialgebraic foundations for the operational semantics of string diagrams, Counting nondeterministic computations, A thesis for interaction, Optimal modular control of discrete event systems with distinguishers and approximations, CCS: it's not fair! Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions, Program equivalence in linear contexts, On labeled birooted tree languages: algebras, automata and logic, Hierarchical modelling of manufacturing systems using discrete event systems and the conflict preorder, Denotational fixed-point semantics for constructive scheduling of synchronous concurrency, Stepwise refinement of sequence diagrams with soft real-time constraints, A structural transformation from p-\(\pi\) to MSVL, The combined use of the web ontology language (OWL) and abstract state machines (ASM) for the definition of a specification language for business processes, Modelling and analysing neural networks using a hybrid process algebra, Automata-theoretic semantics of idealized Algol with passive expressions, Timed process calculi with deterministic or stochastic delays: commuting between durational and durationless actions, A non-SOS operational semantics for a process algebra, Concurrent abstract state machines, Modelling and verifying the AODV routing protocol, Rigorous development of component-based systems using component metadata and patterns, Contextual equivalences in configuration structures and reversibility, Conflict-preserving abstraction of discrete event systems using annotated automata, Two-thirds simulation indexes and modal logic characterization, Behavioural equivalences of a probabilistic pi-calculus, Bisimulation on speed: Worst-case efficiency, Nested semantics over finite trees are equationally hard, A comparison of semantic models for noninterference, A distributed resource allocation algorithm for many processes, Incompleteness of relational simulations in the blocking paradigm, Testing probabilistic equivalence through reinforcement learning, Processes with infinite liveness requirements, A process algebra framework for multi-scale modelling of biological systems, A cylinder computation model for many-core parallel computing, Translating FSP into LOTOS and networks of automata, Model of distributed computing system operation with time, An algebraic theory of interface automata, Specifying termination in CSP, Divide and congruence: from decomposition of modal formulas to preservation of branching and \(\eta \)-bisimilarity, The sweep-line state space exploration method, Value-passing CCS with noisy channels, Connectors as designs: modeling, refinement and test case generation, Rule formats for determinism and idempotence, Totality in arena games, Correct transformation: from object-based graph grammars to PROMELA, Transforming web services choreographies with priorities and time constraints into prioritized-time colored Petri nets, Mechanical reasoning about families of UTP theories, SAT-solving in CSP trace refinement, Timed mobility in process algebra and Petri nets, Structural operational semantics through context-dependent behaviour, Model checking time-dependent system specifications using time stream Petri nets and \texttt{UPPAAL}, From control law diagrams to Ada via \textsf{Circus}, Thread algebra for poly-threading, Observable behavior of distributed systems: component reasoning for concurrent objects, A dynamic deontic logic for complex contracts, Static analysis of IMC, The infinite evolution mechanism of \(\epsilon\)-bisimilarity, Book review of: Robin Sharp, Principles of protocol design, Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language, Domain science and engineering from computer science to the sciences of informatics. II: Science, A sound and complete reasoning system for asynchronous communication with shared futures, Formal communication elimination and sequentialization equivalence proofs for distributed system models, Reasoning about orchestrations of web services using partial correctness, Model checking RAISE applicative specifications, Threaded behavior protocols, Efficient verification of distributed real-time systems with broadcasting behaviors, Hume box calculus: Robust system development through software transformation, Parameter synthesis for hierarchical concurrent real-time systems, Denotational linear time semantics and sequential composition, Models for concurrency: Towards a classification, Probabilistic communicating processes, A complete axiomatization of timed bisimulation for a class of timed regular behaviours, Multi-parameterised compositional verification of safety properties, A parallel algorithm for static program slicing, The weakest deadlock-preserving congruence, Computable concurrent processes, A brief history of Timed CSP, Probabilistic and prioritized models of timed CSP, A process algebraic view of input/output automata, Compositional synthesis of supervisors in the form of state machines and state maps, Computing maximal weak and other bisimulations, Modeling concurrency with interval traces, Petri games: synthesis of distributed systems with causal memory, Structure of concurrency, Modal logics for mobile processes, The expressive power of implicit specifications, Universal axioms for bisimulations, Observing localities, Computational interpretations of linear logic, Graph rewriting for a partial ordering semantics of concurrent constraints programming, Deriving graphical representations of process networks from algebraic expressions, Manifest domains: analysis and description, Refining autonomous agents with declarative beliefs and desires, Specification techniques for Markov reward models, Algorithms for task allocation in ants. (A study of temporal polyethism: Theory), Communicating processes with value-passing and assignments, Mitigating covert channels based on analysis of the potential for communication, Enabling synchronous and asynchronous communications in CSP for SOC, Contexts, refinement and determinism, A tactic language for refinement of state-rich concurrent specifications, Constraint-based analysis of concurrent probabilistic hybrid systems: an application to networked automation systems, On the axiomatizability of priority. II, SOS rule formats for zero and unit elements, Derivation tree analysis for accelerated fixed-point computation, Safe reasoning with logic LTS, Concurrent Kleene algebra and its foundations, Changing system interfaces consistently: a new refinement strategy for CSP\(\|\)B, A semantics for behavior trees using CSP with specification commands, A principled exploration of coordination models, Using data-independence in the analysis of intrusion detection systems, The pursuit of deadlock freedom, Fixed point equations with parameters in the projective model, An axiomatic treatment of SIMD assignment, A framework for compositional nonblocking verification of extended finite-state machines, An exercise in the automatic verification of asynchronous designs, Recursion induction for real-time processes, Process algebra with guards: Combining hoare logic with process algebra, A semantic characterization for faults in replicated systems, A specification-oriented semantics for the refinement of real-time systems, GSOS and finite labelled transition systems, Supervisory control using variable lookahead policies, A fully abstract trace model for dataflow and asynchronous networks, On sequential composition, action prefixes and process prefix, Natural discrete-event process forecasting: A decision support system, Refinement of events in the development of real-time distributed systems, Proofs as processes, Processes with probabilities, priority and time, Automatizing parametric reasoning on distributed concurrent systems, Using integer programming to verify general safety and liveness properties, A polynomial algorithm for deciding bisimilarity of normed context-free processes, Actors, actions, and initiative in normative system specification, Verifying a distributed list system: A case history, Designing equivalent semantic models for process creation, Two implementation relations and the correctness of communicating replicated processes, Time-abstracted bisimulation: Implicit specifications and decidability, A timed model for communicating sequential processes, SIMD language design using prescriptive semantics, A class of non-deterministic specifications for supervisory control, Semantics and verification of monitors and systems of monitors and processes, A state-based approach to communicating processes, Metric semantics for concurrency, An equational axiomatization for multi-exit iteration, The difference between splitting in \(n\) and \(n+1\), On supervisory control of real-time discrete-event systems, The equational theory of pomsets, Introduction to the theory of nested transactions, A complete axiomatization of finite-state ACSR processes, Quiescence, fairness, testing, and the notion of implementation, Running programs backwards: The logical inversion of imperative computation, Type theory and concurrency, Complexity of equivalence problems for concurrent systems of finite agents, A process-calculus-based abstraction for coordinating multi-agent groups, A tutorial on EMPA: A theory of concurrent processes with nondeterminism, priorities, probabilities and time, Fairness and control in multi-agent systems, A process algebra of communicating shared resources with dense time and priorities, The equational logic of fixed points, Notes on the methodology of CCS and CSP, Two finite specifications of a queue, Constructing process categories, An incremental specification of the sliding-window protocol, Design and verification of fault tolerant systems with CSP, Correctness of concurrent processes, Algebraic and fixed point equations over inverse limits of algebras, Specification styles in distributed systems design and verification, Connectedness and synchronization, A proof system for communicating processes with value-passing, Minimizing the number of transitions with respect to observation equivalence, An agent calculus with simple actions where the enabling and disabling are derived operators, Concurrent regular expressions and their relationship to Petri nets, Semantics for data parallel computation, A model of reconfiguration in communicating sequential processes with a notion of transactions, On controllability and normality of discrete event dynamical systems, Conditional rewriting logic as a unified model of concurrency, The chemical abstract machine, An algebraic approach to supervisory control, Temporal theories as modularisation units for concurrent system specification, Specifying modules to satisfy interfaces: A state transition system approach, Experimenting with process equivalence, Causal automata, A compositional axiomatization of statecharts, A calculus of mobile processes. I, Complete sets of axioms for finite basic LOTOS behavioural equivalences, Sequential to parallel buffer refinement, Multitraces, hypertraces and partial order semantics, An algebra for process creation, TIC: a tImed calculus, LOTOS extended with probabilistic behaviours, Semantics of distributed definite clause programs, The semantics of the combination of atomized statements and parallel choice, Verified compilation of communicating processes into clocked circuits, Liveness in timed and untimed systems, A formal approach to the integration of performance aspects in the modeling and analysis of concurrent systems, An invitation to friendly testing, A conservative look at operational semantics with variable binding, Operational and denotational semantics for the box algebra, The timed failures -- Stability model for CSP, A complete equational axiomatization for MPA with string iteration, A process algebra with distributed priorities, Reasoning about nondeterministic and concurrent actions: A process algebra approach, A calculus for cryptographic protocols: The spi calculus, A general theory of action languages, Basic observables for processes, Distributed games, On deciding trace equivalences for processes, A complete modal proof system for HAL: the Herbrand agent language, An abstract machine for concurrent modular systems: CHARM, A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol, Nondeterminacy and recursion via stacks and games, Object inheritance beyond subtyping, The connection between an event structure semantics and an operational semantics for TCSP, Infinitary parallelism without unbounded nondeterminism in CSP, An efficiency preorder for processes, Composition laws for entropy and temperature in tree-like graphs, Axiomatic-like performance analysis (ALPA), An algebraic hardware/software partitioning algorithm, Process languages with discrete relative time based on the ordered SOS format and rooted eager bisimulation, A UTP approach for rTiMo, Combining static analysis and case-based search space partitioning for reducing peak memory in model checking, A fixpoint theory for non-monotonic parallelism, Power simulation and its relation to traces and failures refinement, Tracking CSP computations, Compositional refinements in multiple blackboard systems, A secrecy-preserving language for distributed and object-oriented systems, Modularizing behavioral and architectural crosscutting concerns in formal component-based systems -- application to the behavior interaction priority framework, Compositional failure-based semantic models for basic LOTOS, Interpreting message flow graphs, On simulation, subtyping and substitutability in sequential object systems, A theory of Orwellian specifications with NewThink, Semantics of under-determined expressions, Architectural CCS, Discrete time process algebra, Retargeting a hardware compiler using protocol converters, Approximate analyzing of labeled transition systems, Stochastic modelling of diffusion equations on a parallel machine, Timing and causality in process algebra, Designing a semantic model for a wide-spectrum language with concurrency, An alternative formulation of operational conservativity with binding terms., Algebraic theory of probabilistic processes., TTL: A modular language for hardware/software systems design., New architectures for constructed complex systems, Testing interruptions in reactive systems, Reconciling real and stochastic time: the need for probabilistic refinement, External and internal choice with event groups in Event-B, Characterisations of testing preorders for a finite probabilistic \(\pi\)-calculus, Probabilistic may/must testing: retaining probabilities by restricted schedulers, Semantic inheritance in unifying theories of programming, Unifying theories in ProofPower-Z, Relating computer systems to sequence diagrams: the impact of underspecification and inherent nondeterminism, On the limits of refinement-testing for model-checking CSP, Complete and ready simulation semantics are not finitely based over BCCSP, even with a singleton alphabet, Quantum process algebra with priorities, A system for compositional verification of asynchronous objects, The symbiosis of concurrency and verification: teaching and case studies, Unifying theories of time with generalised reactive processes, On hierarchically developing reactive systems, Deriving structural labelled transitions for mobile ambients, Hybrid I/O automata., A formal approach to open multiparty interactions, Normative dynamic analysis of extreme operational modes of a heterogeneous computing system, Reducing complex CSP models to traces via priority, Grammar-based model transformations: definition, execution, and quality properties, Compiling and verifying SC-SystemJ programs for safety-critical reactive systems, Rule formats for distributivity, Semantics of non-deterministic possibility computation, CCS with Hennessy's merge has no finite-equational axiomatization, A hierarchy of failures-based models: theory and application, Locating reaction with 2-categories, A brief history of process algebra, On the usability of process algebra: An architectural view, An axiomatic semantics for \(\mathsf{ioco} \underline{\mathsf{s}}\) conformance relation, A logic for the stepwise development of reactive systems, Models and languages for description of parallel processes, A UTP semantics for communicating processes with shared variables and its formal encoding in PVS, Modular specification of process algebras, Locked discrete event systems: How to model and how to unlock, The sliding-window protocol revisited, Progress assumption in concurrent systems, Action systems, unbounded nondeterminism, and infinite traces, A coordination theory for intelligent machines, Action transducers and timed automata, Decentralized supervisory control of discrete-event systems, Bisimulation of automata, Semantic models for information flow, Linda-based applicative and imperative process algebras, Finite axiom systems for testing preorder and De Simone process languages, Delay-insensitivity and ternary simulation, A hidden agenda, ConGolog, a concurrent programming language based on the situation calculus, On a class of timer hybrid systems reducible to finite state automata, Process algebras for systems diagnosis., Analysis of security protocols as open systems, Performance measure sensitive congruences for Markovian process algebras, Discrete time generative-reactive probabilistic processes with different advancing speeds, A new logic for electronic commerce protocols, Contracts, games, and refinement., Bisimilarity of open terms., An algebraic framework for urgency, Inductive synthesis of recursive processes from logical properties, Full abstraction for PCF, Module checking, Synchronization languages and rewriting systems, Objects and classes in Algol-like languages, The box algebra = Petri nets + process expressions, Ordered SOS process languages for branching and eager bisimulations, Finite-state analysis of two contract signing protocols, The theory of interactive generalized semi-Markov processes, CSP, partial automata, and coalgebras., Resource traces: A domain for processes sharing exclusive resources., A causal semantics for CCS via rewriting logic, The music of streams, The cones and foci proof technique for timed transition systems, Additive models of probabilistic processes, Comparing logics for rewriting: Rewriting logic, action calculi and tile logic, Actor theories in rewriting logic, Proving the validity of equations in GSOS languages using rule-matching bisimilarity, Compositional Modelling and Reasoning in an Institution for Processes and Data, The Equational Theory of Weak Complete Simulation Semantics over BCCSP, Nondeterministic modal interfaces, Modeling for Verification, Process Algebra and Model Checking, Stochastic equivalence for performance analysis of concurrent systems in dtsiPBC, A Truly Concurrent Process Semantics over Multi-Pomsets of Consumable Resources, Behavioural Models for FMI Co-simulations, Unifying Heterogeneous State-Spaces with Lenses, Extending modal transition systems with structured labels, Nondeterministic probabilistic Petri net -- a new method to study qualitative and quantitative behaviors of system, Deadlock analysis in networks of communicating processes, Determinism \(\to\) (event structure isomorphism \(=\) step sequence equivalence), Highly concurrent logically synchronous multicast, Transformations of sequential specifications into concurrent specifications by synchronization guards, A domain equation for bisimulation, The laws of Occam programming, Responsiveness and stable revivals, Interactive tool support for CSP \(\parallel\) B consistency checking, Reversing algebraic process calculi, Formal analysis of composable DeFi protocols, Fairness and communication-based semantics for session-typed languages, rCOS: Defining Meanings of Component-Based Software Architectures, Unifying Theories of Programming in Isabelle, Reactive bisimulation semantics for a process algebra with timeouts, Decomposing monolithic processes in a process algebra with multi-actions, Models for CSP with availability information, Lattice-valued Scott topology on dcpos, Symbolic Semantics for Multiparty Interactions in the Link-Calculus, A New Roadmap for Linking Theories of Programming, Towards a UTP Semantics for Modelica, UTP Semantics of Reactive Processes with Continuations, Compositionality issues in discrete, continuous, and hybrid systems, Topological Construction of Parameterized Bisimulation Limit, Relational Concurrent Refinement: Automata, Of wlp and CSP, Simulating Truly Concurrent CSP, Graph Generation to Statically Represent CSP Processes, The compositional construction of Markov processes II, Simulating asynchronous hardware on multiprocessor platforms: the case of AMULET1, FSP and FLTL framework for specification and verification of middle-agents, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Verifying security protocols with PVS: widening the rank function approach, Pure bigraphs: structure and dynamics, Fairness of components in system computations, Branching bisimulation for probabilistic systems: characteristics and decidability, Leader election in rings of ambient processes, On testing UML statecharts, Fairness of actions in system computations, Failure-based equivalence of constraint automata, Processes as formal power series: a coinductive approach to denotational semantics, An algebraic theory for behavioral modeling and protocol synthesis in system design, Verification of system level model transformations, Connection between logical and algebraic approaches to concurrent systems, Bisimulation for labelled Markov processes, ON FORMAL AND COGNITIVE SEMANTICS FOR SEMANTIC COMPUTING, Systems specification by basic protocols, Declarative Programming with Algebra, Identity-Based Cryptosystems and Quadratic Residuosity, Mitigating Multi-target Attacks in Hash-Based Signatures, BAL Tool in Flexible Manufacturing Systems, A Timed Process Algebra for Wireless Networks with an Application in Routing, The expressiveness of CSP with priority, Refinement Sensitive Formal Semantics of State Machines With Persistent Choice, Compositional Failure-based Equivalence of Constraint Automata, On CSP Refinement Tests That Run Multiple Copies of a Process, Counter Abstraction in the CSP/FDR setting, Three Approaches to Timed External Choice in UTP, Isabelle/UTP: A Mechanised Theory Engineering Framework, Towards Algebraic Semantics of Circus Time, Extending MSVL with Semaphore, Reactive Turing Machines, Static Livelock Analysis in CSP, Probabilistic model of software approximate correctness, Axiomatizing Weak Ready Simulation Semantics over BCCSP, Abstract Interpretation for Proving Secrecy Properties in Security Protocols, Message Sequence Charts in the Development Process — Roles and Limitations, The Value-Passing Calculus, Slow Abstraction via Priority, Towards a Modeling Language for Cyber-Physical Systems, Process synchronisation as fusion, Analyzing a \(\chi\) model of a turntable system using Spin, CADP and Uppaal, \(\pi\)-calculus with noisy channels, Slicing techniques for verification re-use, A theory of stochastic systems. II: Process algebra, Remarks on Testing Probabilistic Processes, Systems Modelling via Resources and Processes: Philosophy, Calculus, Semantics, and Logic, Observable Behavior of Dynamic Systems: Component Reasoning for Concurrent Objects, Simulations Up-to and Canonical Preorders, Process Algebra Having Inherent Choice: Revised Semantics for Concurrent Systems, A Calculus for Team Automata, Type Checking Specifications, Automatic Verification of Combined Specifications: An Overview, The semantics and verification of timed service choreography, REGULAR STATE MACHINES, Holistic Specifications for Robust Programs, Towards Bridging Time and Causal Reversibility, On relating some models for concurrency, A case study in transformational design of concurrent systems, From π-calculus to higher-order π-calculus — and back, A technique for specifying and refining TCSP processes by using guards and liveness conditions, Constructing systems as object communities, Testability of a communicating system through an environment, Property preserving abstractions under parallel composition, Unifying models, Evaluation Trees for Proposition Algebra, Structure Preserving Bisimilarity, Supporting an Operational Petri Net Semantics of CCSP, Supervisory control of concurrent discrete-event systems, KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS, A duration calculus with infinite intervals, Bounded concurrency, Change impact analysis to support architectural evolution, Dynamic Logic with Binders and Its Application to the Development of Reactive Systems, Transputers for solving any system of linear equations, Argumentation through a distributed self-stabilizing approach, Reasoning About Resources in the Embedded Systems Language Hume, Asynchronous Traces and Open Petri Nets, Language Representability of Finite P/T Nets, Quantales, observational logic and process semantics, Step bisimulation is pomset equivalence on a parallel language without explicit internal choice, Testing Finitary Probabilistic Processes, Concurrent Kleene Algebra, Property Preserving Refinement for Csp-Casl, ON THE PARALLEL AND PERPENDICULAR COMPUTATIONS, Joyce—A programming language for distributed systems, A mathematical model for system design and refinement, Order algebras: a quantitative model of interaction, Sheaf semantics for concurrent interacting objects, Discrete events and general systems theory, Unnamed Item, The Subject-Oriented Approach to Software Design and the Abstract State Machines Method, Enriched μ–Calculus Pushdown Module Checking, PROPOSITIONAL DYNAMIC LOGIC FOR REASONING ABOUT FIRST-CLASS AGENT INTERACTION PROTOCOLS, Neural networks and adaptive expert systems in the CSA approach, Twenty Years on: Reflections on the CEDISYS Project. Combining True Concurrency with Process Algebra, Branching vs. Linear Time: Semantical Perspective, The Birth of Model Checking, On the stability of asynchronous iterative processes, A self-modifiable approach to scheduling and mapping algorithms in multiprocessor systems, Compositional Modeling and Minimization of Time-Inhomogeneous Markov Chains, An interpreter for LOTOS, a specification language for distributed systems, Unnamed Item, On the Purpose of Event-B Proof Obligations, Unnamed Item, Unnamed Item, Unnamed Item, Formal Analysis of Model Transformations Based on Triple Graph Rules with Kernels, A Notion of Glue Expressiveness for Component-Based Systems, Unnamed Item, On the interpretation of mathematical entities in the formalisation of programming and modelling languages, A ground-complete axiomatisation of finite-state processes in a generic process algebra, Efficient analysis of concurrent constraint logic programs, New algebraic methods for modelling large‐scale integrated circuits, Compositionality in state space verification methods, Reduced state space representation for unbounded vector state spaces, Behavioural equivalence for infinite systems — Partially decidable!, The Automatic Detection of Token Structures and Invariants Using SAT Checking, A domain for concurrent termination a generalization of Mazurkiewicz traces, Solving recursive net equations, Process specification and verification, The decomposition of ESM computations, On the operating unit size of load/store architectures, ON THE PERFORMANCE AND COST OF SOME PRAM MODELS ON CMP HARDWARE, Hyperformulae, Parallel Deductions and Intersection Types, Embedding Untimed into Timed Process Algebra; the Case for Explicit Termination, The Two-Phase Commitment Protocol in an Extended π-Calculus, Process Calculi à la Bird-Meertens, A constant time string shuffle algorithm on reconfigurable meshes, Behavioral Constraints for Visual Models1 1Research partially supported by the ESPRIT Working Group APPLIGRAPH and the TMR network GETGRATS., Diagrammatic Reasoning for Delay-Insensitive Asynchronous Circuits, Refinement-Preserving Plug-In Components, Safe Reasoning with Logic LTS, Teaching Concurrency Concepts to Freshmen, Unnamed Item, Changing System Interfaces Consistently: A New Refinement Strategy for CSP||B, CSP with Hierarchical State, Modelling Divergence in Relational Concurrent Refinement, Model Checking LTL Formulae in RAISE with FDR, Effective Representation of RT-LOTOS Terms by Finite Time Petri Nets, Distributed processes and location failures, Modeling Routing Protocols in Adhoc Networks, Comparing State Spaces in Automatic Security Protocol Analysis, A Process-Model for Linear Programs, Process Algebra Modelling Styles for Biomolecular Processes, SC-EXPRESSIONS IN OBJECT-ORIENTED LANGUAGES, Formal Verification for High-Assurance Behavioral Synthesis, An expressiveness study of priority in process calculi, On Communicating Finite-State Machines, Unnamed Item, AXIOMATIC FRAMEWORKS FOR DEVELOPING BSP-STYLE PROGRAMS∗, Specifications in stochastic process algebra for a robot control problem, Computational Probabilistic Non-interference, Analysing a Stream Authentication Protocol Using Model Checking, Equal To The Task?, Testing probabilistic automata, Extended Markovian Process Algebra, Synchronous development of asynchronous systems, Automatic generation of verified concurrent hardware using VHDL, Trade-offs in true concurrency: Pomsets and mazurkiewicz traces, On relating concurrency and nondeterminism, Jifeng He at Oxford and beyond: an appreciation, Intuitive modelling and formal analysis of collective behaviour in foraging ants, Modular rewritable Petri nets: an efficient model for dynamic distributed systems, Neighbourhood message passing computation on a lattice with cP systems, Bridging Causal Reversibility and Time Reversibility: A Stochastic Process Algebraic Approach, Distribution-based limited fuzzy bisimulations for nondeterministic fuzzy transition systems, Back to the format: a survey on SOS for probabilistic processes, Formally verified animation for RoboChart using interaction trees, Analysing AWN-Specifications Using mCRL2 (Extended Abstract), Non-finite axiomatisability results via reductions: CSP parallel composition and CCS restriction, Fair must testing for I/O automata, A contract-based semantics and refinement for Simulink, Equations for if-then-else, Correct and efficient antichain algorithms for refinement checking, On the Introduction of Guarded Lists in Bach: Expressiveness, Correctness, and Efficiency Issues, Unnamed Item, Distributed Adaptive Systems, A generalized Kahn Principle for abstract asynchronous networks, A hierarchy of domains for real-time distributed computing, Factorizing proofs in timed CSP, Unbounded nondeterminism in CSP, Termination, deadlock and divergence, Categorical semantics for programming languages, Final universes of processes, Topological models for higher order control flow, Time abstracted bisimulation: Implicit specifications and decidability, Axiomatising real-timed processes, Compositional process semantics of Petri Boxes, EditorArrow: An arrow-based model for editor-based programming, Bisimulation on speed: Lower time bounds, Unnamed Item, Unnamed Item, Unnamed Item, Towards a complete hierarchy of compositional dataflow models, Graph-grammar semantics of a higher-order programming language for distributed systems, An algebraic semantics for hierarchical P/T nets, Causal behaviours and nets, An algebraic framework for developing and maintaining real-time systems, A Calculus of Countable Broadcasting Systems, CSP and anonymity, Generated models and the ω-rule: The nondeterministic case, A functorial semantics for observed concurrency, Read-write causality, A Unary Semigroup Trace Algebra, Interleaving vs True Concurrency: Some Instructive Security Examples, When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus, Cyclic vector languages, An algebraic theory of multiple clocks, High level expressions with their SOS semantics, On implementations and semantics of a concurrent programming language, Translation of CCS into CSP, correct up to strong bisimulation, Modelling mutual exclusion in a process algebra with time-outs, A survey on compositional algorithms for verification and synthesis in supervisory control, Semantics of dynamic hiding in mobile UTP-CSP, Model checking meets auto-tuning of high-performance programs, Retracing some paths in process algebra, Comparing transition systems with independence and asynchronous transition systems, Unnamed Item, Verifying Optimizations for Concurrent Programs, Calculational derivation of a counter with bounded response time and bounded power dissipation, Wait-free linearization with a mechanical proof, Generating diagnostic information for behavioral preorders, Design and analysis of dynamic leader election protocols in broadcast networks, Timewise refinement for communicating processes, Linking Event-B and Concurrent Object-Oriented Programs, More Relational Concurrent Refinement: Traces and Partial Relations, General Refinement, Part One: Interfaces, Determinism and Special Refinement, General Refinement, Part Two: Flexible Refinement, A process algebra with distributed priorities, Explicit Identifiers and Contexts in Reversible Concurrent Calculus, Separation Logic Semantics for Communicating Processes, Branching Bisimulation Congruence for Probabilistic Systems, A Programming Language for Spatial Distribution of Net Systems, Variable binding operators in transition system specifications, Combining termination proofs in model transformation systems, On recursive operations over logic LTS, Relating reasoning methodologies in linear logic and process algebra, CSP-CASL-Prover: A Generic Tool for Process and Data Refinement, PVS Embedding of cCSP Semantic Models and Their Relationship, The Stable Revivals Model in CSP-Prover, The ARC Programming Model – Language Constructs for Coordination, Refactoring Object-Oriented Specifications with Data and Processes, Quantales, finite observations and strong bisimulation, Algebraic characterizations of trace and decorated trace equivalences over tree-like structures, Inheritance of behavior, Real time process algebra with time-dependent conditions, Synchronous Message Passing: On the Relation between Bisimulation and Refusal Equivalence, Unnamed Item, Unnamed Item, An introduction to compositional methods for concurrency and their application to real-time., Logical models of discrete even systems: a comparative exposition, Non-regular iterators in process algebra, Refinement and state machine abstraction, Divergence in testing and readiness semantics, Distributed processes and location failures, Kleene Theorems for Product Systems, Interleaving Strategies, Checking equivalences between concurrent systems of finite agents (Extended abstract), Finite-state concurrent programs can be expressed in pairwise normal form, A survey of modal logics characterising behavioural equivalences for non-deterministic and stochastic systems, Maurer computers for pipelined instruction processing, Unnamed Item, Unnamed Item, Equations, Contractions, and Unique Solutions, An efficiency preorder for processes, CONFLICTS AND FAIR TESTING, A TIMED FAILURE EQUIVALENCE PRESERVING ABSTRACTION FOR PARAMETRIC TIME-INTERVAL AUTOMATA, Journeys in non-classical computation I: A grand challenge for computing research, Optimal Supervisory Control of Discrete Event Systems: Cyclicity and Interleaving of Tasks, Simplified Coalgebraic Trace Equivalence, Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP, Quantifying Probabilistic Information Flow in Computational Reactive Systems, A Generic Process Algebra, Retracing CSP, A Family of Resource-Bound Real-Time Process Algebras, Operational Semantics of Reversibility in Process Algebra