scholarly journals Transition Systems with Independence and Multi-Arcs

1997 ◽  
Vol 4 (10) ◽  
Author(s):  
Thomas Troels Hildebrandt ◽  
Vladimiro Sassone
Keyword(s):  
Concurrent Systems ◽  
Transition Systems

We extend the model of transition systems with independence in order to provide it with a feature relevant in the noninterleaving analysis of concurrent systems, namely multi-arcs. Moreover, we study the relationships between the category of transition systems with independence and multi-arcs and the category of labeled asynchronous transition systems, extending the results recently obtained by the authors for (simple) transition systems with independence (cf. Proc. CONCUR’96), and yielding a precise characterisation of transition systems with independence and multi-arcs in terms of (event-maximal, diamond-extensional) labelled asynchronous transition systems.

CONCURRENT AUTOMATA AND DOMAINS

1992 ◽  
Vol 03 (04) ◽  
pp. 389-418 ◽  
Author(s):  
MANFRED DROSTE
Keyword(s):  
Concurrent Systems ◽  
Equivalence Classes ◽  
Binary Relations ◽  
Transition Systems ◽  
Operational Model ◽  
Locally Finite ◽  
Natural Domain ◽  
Theoretic Characterization ◽  
Natural Way

We introduce an operational model of concurrent systems, called automata with concurrency relations. These are labeled transition systems [Formula: see text] in which the event set is endowed with a collection of symmetric binary relations which describe when two events at a particular state of [Formula: see text] commute. This model generalizes the recent concept of Stark’s trace automata. A permutation equivalence for computation sequences of [Formula: see text] arises canonically, and we obtain a natural domain [Formula: see text] comprising the induced equivalence classes. We give a complete order-theoretic characterization of all such partial orders [Formula: see text] which turn out to be particular finitary domains. The arising domains [Formula: see text] are particularly pleasant Scott-domains, if [Formula: see text] is assumed to be concurrent, i.e. if the concurrency relations of [Formula: see text] depend (in a natural way) locally on each other, but not necessarily globally. We show that both event domains and dI-domains arise, up to isomorphism, as domains [Formula: see text] with well-behaved such concurrent automata [Formula: see text]. We introduce a subautomaton relationship for concurrent automata and show that, given two concurrency domains (D, ≤), (D′, ≤), there exists a nice stable embedding-projection pair from D to D′ iff D, D′ can be generated by concurrent automata [Formula: see text] such that [Formula: see text] is a subautomaton of [Formula: see text]. Finally, we introduce the concept of locally finite concurrent automata as a limit of finite concurrent automata and show that there exists a universal homogeneous locally finite concurrent automaton, which is unique up to isomorphism.

Hidden coinduction: behavioural correctness proofs for objects

1999 ◽  
Vol 9 (3) ◽  
pp. 287-319 ◽  
Author(s):  
JOSEPH A. GOGUEN ◽  
GRANT MALCOLM
Keyword(s):  
Software Engineering ◽  
Concurrent Systems ◽  
Functional Constraint ◽  
Transition Systems ◽  
Correctness Proofs ◽  
General Goals ◽  
Future Plans

This paper unveils and motivates an ambitious programme of hidden algebraic research in software engineering. We begin with an outline of our general goals, continue with an overview of results, and conclude with a discussion of some future plans. The main contribution is powerful hidden coinduction techniques for proving behavioural correctness of concurrent systems, and several mechanical proofs are given using OBJ3. We also show how modularization, bisimulation, transition systems, concurrency and combinations of the functional, constraint, logic and object paradigms fit into hidden algebra.

Multiple-Labelled Transition Systems for nominal calculi and their logics

2008 ◽  
Vol 18 (1) ◽  
pp. 107-143 ◽  
Author(s):  
ROCCO DE NICOLA ◽  
MICHELE LORETI
Keyword(s):  
Mobile Computing ◽  
Concurrent Systems ◽  
Distributed Environment ◽  
Transition Systems ◽  
Semantic Framework ◽  
Labelled Transition Systems ◽  
Fundamental Model ◽  
Π Calculus ◽  
The Impact

Action-labelled transition systems (LTSs) have proved to be a fundamental model for describing and proving properties of concurrent systems. In this paper we introduce Multiple-Labelled Transition Systems (MLTSs) as generalisations of LTSs that enable us to deal with system features that are becoming increasingly important when considering languages and models for network-aware programming. MLTSs enable us to describe not only the actions that systems can perform but also their usage of resources and their handling (creation, revelation . . .) of names; these are essential for modelling changing evaluation environments. We also introduce MoMo, which is a logic inspired by Hennessy–Milner Logic and the μ-calculus, that enables us to consider state properties in a distributed environment and the impact of actions and movements over the different sites. MoMo operators are interpreted over MLTSs and both MLTSs and MoMo are used to provide a semantic framework to describe two basic calculi for mobile computing, namely μKlaim and the asynchronous π-calculus.

From Process Models to Concurrent Systems in Alvis Language

Informatica ◽  
2017 ◽  
Vol 28 (3) ◽  
pp. 525-545 ◽  
Author(s):  
Marcin Szpyrka ◽  
Grzegorz J. Nalepa ◽  
Krzysztof Kluza
Keyword(s):  
Concurrent Systems ◽  
Process Models

Neural Transition Systems for Modeling Hierarchical Semantic Representations

2019 ◽  
Author(s):  
Riyaz Bhat ◽  
John Chen ◽  
Rashmi Prasad ◽  
Srinivas Bangalore
Keyword(s):  
Semantic Representations ◽  
Transition Systems

Gender from Latin to Romance

2018 ◽  
Author(s):  
Michele Loporcaro
Keyword(s):  
Grammatical Gender ◽  
Concurrent Systems ◽  
Fundamental Question ◽  
Romance Languages ◽  
Back Projection ◽  
Linguistic Typology ◽  
Romance Language ◽  
Dialect Variation ◽  
Main Culprit ◽  
Gender System

The book addresses grammatical gender in Romance, and its development from Latin. It works with the toolbox of current linguistic typology, and asks the fundamental question of how the Latin grammatical gender system gradually changed into those of the Romance languages. To answer this question, the book capitalizes on the pervasive dialect variation of which the better-known standard Romance languages only represent a fragment. Indeed, inspection of dialect variation across time and space forces one to dismiss the handbook account proclaiming that the neuter gender, contrasting with masculine and feminine in Latin, was eradicated from spoken Latin by late Empire times. Both Late Latin evidence and data from several modern dialects show that this never happened, and that the vulgate account proceeds from unwarranted back-projection of the data from modern languages like French and Italian. Rather, the neuter underwent transformations which are the main culprit for the differences in the gender system observed today between, say, Romanian, Sursilvan, Neapolitan, and Asturian, to cite just a few types of system which turn out to differ significantly. A precondition for establishing the database for diachronic investigation is a detailed description of many such systems, which reveals data whose interest transcends the diachronic issue under consideration: the book thus addresses systems where ‘husbands’ are feminine and others where ‘wives’ are masculine; discusses dialects where nouns overtly mark gender, but only in certain syntactic contexts; and proposes an analysis according to which one Romance language (Asturian) has split inherited grammatical gender into two concurrent systems.

scholarly journals Battery transition systems

2014 ◽  
Vol 49 (1) ◽  
pp. 595-606 ◽  
Author(s):  
Udi Boker ◽  
Thomas A. Henzinger ◽  
Arjun Radhakrishna
Keyword(s):  
Transition Systems

The Complexity of Model-Checking Tail-Recursive Higher-Order Fixpoint Logic

2021 ◽  
Vol 178 (1-2) ◽  
pp. 1-30
Author(s):  
Florian Bruse ◽  
Martin Lange ◽  
Etienne Lozes
Keyword(s):  
Model Checking ◽  
Lower Bounds ◽  
Expressive Power ◽  
Higher Order ◽  
Order Logic ◽  
High Complexity ◽  
Transition Systems ◽  
Recursive Formulas ◽  
Second Order Logic ◽  
Monadic Second Order Logic

Higher-Order Fixpoint Logic (HFL) is a modal specification language whose expressive power reaches far beyond that of Monadic Second-Order Logic, achieved through an incorporation of a typed λ-calculus into the modal μ-calculus. Its model checking problem on finite transition systems is decidable, albeit of high complexity, namely k-EXPTIME-complete for formulas that use functions of type order at most k < 0. In this paper we present a fragment with a presumably easier model checking problem. We show that so-called tail-recursive formulas of type order k can be model checked in (k − 1)-EXPSPACE, and also give matching lower bounds. This yields generic results for the complexity of bisimulation-invariant non-regular properties, as these can typically be defined in HFL.

Causal-Consistent Replay Reversible Semantics for Message Passing Concurrent Programs

2021 ◽  
Vol 178 (3) ◽  
pp. 229-266
Author(s):  
Ivan Lanese ◽  
Adrián Palacios ◽  
Germán Vidal
Keyword(s):  
Programming Language ◽  
Message Passing ◽  
Concurrent Programming ◽  
Concurrent Systems ◽  
Concurrent Programs ◽  
Unified Framework ◽  
Innovative Technique ◽  
Dual Notion

Causal-consistent reversible debugging is an innovative technique for debugging concurrent systems. It allows one to go back in the execution focusing on the actions that most likely caused a visible misbehavior. When such an action is selected, the debugger undoes it, including all and only its consequences. This operation is called a causal-consistent rollback. In this way, the user can avoid being distracted by the actions of other, unrelated processes. In this work, we introduce its dual notion: causal-consistent replay. We allow the user to record an execution of a running program and, in contrast to traditional replay debuggers, to reproduce a visible misbehavior inside the debugger including all and only its causes. Furthermore, we present a unified framework that combines both causal-consistent replay and causal-consistent rollback. Although most of the ideas that we present are rather general, we focus on a popular functional and concurrent programming language based on message passing: Erlang.

Sign in / Sign up

Export Citation Format

Share Document