Who is obliged when many are involved? Labelled transition system modelling of how obligation arises

Polish Law ◽

The Right ◽

AbstractThe paper tackles the problem of the relation between rights and obligations. Two examples of situations in which such a relation occurs are discussed. One concerns the abortion regulations in Polish law, the other one—a clash between freedom of expression and freedom of enterprise occurring in the context of discrimination. The examples are analysed and formalised using labelled transition systems in the $$n\mathcal {C}+$$ n C + framework. Rights are introduced to the system as procedures allowing for their fulfilment. Obligations are based on the requirement of cooperation in the realisation of the goals of the agent that has a right. If the right of an agent cannot be fulfilled without an action of another agent, then that action is obligatory for that agent. If there are many potential contributors who are individually allowed to refuse, then the last of them is obliged to help when all the others have already refused. By means of formalisation this account of the relation under consideration is precisely expressed and shown consistent.

Relating Apartness and Bisimulation

Logical Methods in Computer Science ◽

10.46298/lmcs-17(3:15)2021 ◽

2021 ◽

Vol Volume 17, Issue 3 ◽

Author(s):

Herman Geuvers ◽

Bart Jacobs

Keyword(s):

Transition System ◽

Proof System ◽

Transition Systems ◽

Induction Principle ◽

Weak Bisimulation ◽

Initial Algebra ◽

Branching Bisimulation ◽

Dual Notion ◽

A bisimulation for a coalgebra of a functor on the category of sets can be described via a coalgebra in the category of relations, of a lifted functor. A final coalgebra then gives rise to the coinduction principle, which states that two bisimilar elements are equal. For polynomial functors, this leads to well-known descriptions. In the present paper we look at the dual notion of "apartness". Intuitively, two elements are apart if there is a positive way to distinguish them. Phrased differently: two elements are apart if and only if they are not bisimilar. Since apartness is an inductive notion, described by a least fixed point, we can give a proof system, to derive that two elements are apart. This proof system has derivation rules and two elements are apart if and only if there is a finite derivation (using the rules) of this fact. We study apartness versus bisimulation in two separate ways. First, for weak forms of bisimulation on labelled transition systems, where silent (tau) steps are included, we define an apartness notion that corresponds to weak bisimulation and another apartness that corresponds to branching bisimulation. The rules for apartness can be used to show that two states of a labelled transition system are not branching bismilar. To support the apartness view on labelled transition systems, we cast a number of well-known properties of branching bisimulation in terms of branching apartness and prove them. Next, we also study the more general categorical situation and show that indeed, apartness is the dual of bisimilarity in a precise categorical sense: apartness is an initial algebra and gives rise to an induction principle. In this analogy, we include the powerset functor, which gives a semantics to non-deterministic choice in process-theory.

Target-oriented Petri Net Synthesis

A Mosaic of Computational Topics: from Classical to Novel ◽

10.3233/stal200007 ◽

2020 ◽

Author(s):

Eike Best ◽

Raymond Devillers ◽

Evgeny Erofeev ◽

Harro Wimmel

Keyword(s):

Petri Nets ◽

Petri Net ◽

Transition System ◽

Efficient Synthesis ◽

Transition Systems ◽

Np Complete ◽

Full Class ◽

Petri Net Synthesis ◽

Labelled Transition System ◽

Additional Constraints

When a Petri net is synthesised from a labelled transition system, it is frequently desirable that certain additional constraints are fulfilled. For example, in circuit design, one is often interested in constructing safe Petri nets. Targeting such subclasses of Petri nets is not necessarily computationally more efficient than targeting the whole class. For example, targeting safe nets is known to be NP-complete while targeting the full class of place/transition nets is polynomial, in the size of the transition system. In this paper, several classes of Petri nets are examined, and their suitability for being targeted through efficient synthesis from labelled transition systems is studied and assessed. The focus is on choice-free Petri nets and some of their subclasses. It is described how they can be synthesised efficiently from persistent transition systems, summarising and streamlining in tutorial style some of the authors’ and their groups’ work over the past few years.

Labelled transition system approach to distributed computing systems

Journal of Computer Science and Cybernetics ◽

10.15625/1813-9663/8/3/8272 ◽

2016 ◽

Vol 8 (3) ◽

pp. 19-32

Author(s):

Dang Van Hung

Keyword(s):

Distributed Computing ◽

System Approach ◽

Transition System ◽

Distributed Computing Systems ◽

Computing Systems ◽

Transition Systems ◽

Local Process ◽

Global Properties ◽

The present paper introduces the notion of distributed transition systems for modeling, designing and understanding distributed computing systems. The concurrency can be expressed explicitly in the model. Some of the global properties of the systems are discussed and determined. It is shown in the paper that by keeping knowledge of other processes in each process of a system, some of its global properties can be synthesized from only few local process states.

Foundations of Modular SOS

BRICS Report Series ◽

10.7146/brics.v6i54.20124 ◽

1999 ◽

Vol 6 (54) ◽

Cited By ~ 8

Author(s):

Peter D. Mosses

Keyword(s):

Programming Languages ◽

Transition System ◽

Transition Systems ◽

A novel form of labelled transition system is proposed, where the labels are the arrows of a category, and adjacent labels in computations are required to be composable. Such transition systems provide the foundations for modular SOS descriptions of programming languages. Three fundamental ways of transforming label categories, analogous to monad transformers, are provided, and it is shown that their applications preserve computations in modular SOS. The approach is illustrated with fragments taken from a modular SOS for ML concurrency primitives.

Transition System Models for Concurrency

DAIMI Report Series ◽

10.7146/dpb.v21i399.6633 ◽

1992 ◽

Vol 21 (399) ◽

Author(s):

Madhavan Mukund

Keyword(s):

Petri Nets ◽

Transition System ◽

Transition Systems ◽

System Models ◽

Elementary Transition ◽

Step Transition ◽

Sequential Behaviour

Labelled transition systems can be extended to faithfully model concurrency by permitting transitions between states to be labelled by a collection of actions, denoting a concurrent step, We can characterize a subclass of these step transition systems, called PN-transition systems, which describe the behaviour of Petri nets.This correspondence is formally described in terms of a coreflection between a category of PN-transition systems and a category of Petri nets.In this paper, we show that we can define subcategories of PN-transition systems whose objects are safe PN-transition systems and elementary PN-transition systems such that there is a coreflection between these subcategories and subcategories of our category of Petri nets corresponding to safe nets and elementary net systems.We also prove that our category of elementary PN-transition systems is equivalent to the category of (sequential) elementary transition systems defined by Nielsen, Rozenberg and Thiagarajan, thereby establishing that the concurrent behaviour of an elementary net system can be completely recovered from a description of its sequential behaviour. Finally, we establish a coreflection between our category of safe PN-transition system and a subcategory of asynchronous transition systems which has been shown by Winskel and Nielsen to be closely linked to safe nets.

Advances in Media, Entertainment, and the Arts - Handbook of Research on Combating Threats to Media Freedom and Journalist Safety ◽

The Pitfalls and Perils of Being a Digital Journalist in Venezuela

10.4018/978-1-7998-1298-2.ch017 ◽

2020 ◽

pp. 319-337

Author(s):

Mariateresa Garrido

Keyword(s):

Digital Media ◽

Freedom Of Expression ◽

Secondary Data ◽

The Other ◽

Freedom Of The Press ◽

The Past ◽

Other Hand ◽

The Press ◽

The One ◽

The Right

To be a journalist in Venezuela is very dangerous. In the past decade, there has been an increase of attacks against media and their personnel. On the one hand, attacks against journalists include harassment (physical, digital, legal), illegal detentions, kidnapping, and assassination. On the other hand, digital media have experienced blockages (DNS), internet shutdowns and slow-downs, failures in the connection, and restrictions to access internet-based platforms and content. Since 2014, the situation is deteriorating and limitations to exercise the right to freedom of expression have increased. However, this issue remains understudied; hence, this chapter considers primary and secondary data to analyze the types of limitations experienced by Venezuelan digital journalists from 2014 to 2018, explains the effects of ambiguous regulations and the use of problematic interpretations, and describes the inadequacies of national policies to promote freedom of the press.

Target-oriented Petri Net Synthesis

Fundamenta Informaticae ◽

10.3233/fi-2020-1949 ◽

2020 ◽

Vol 175 (1-4) ◽

pp. 97-122

Author(s):

Eike Best ◽

Raymond Devillers ◽

Evgeny Erofeev ◽

Harro Wimmel

Keyword(s):

Petri Nets ◽

Circuit Design ◽

Petri Net ◽

Transition System ◽

Transition Systems ◽

Np Complete ◽

Full Class ◽

Petri Net Synthesis ◽

Labelled Transition System ◽

Additional Constraints

A domain equation for refinement of partial systems

Mathematical Structures in Computer Science ◽

10.1017/s0960129504004268 ◽

2004 ◽

Vol 14 (4) ◽

pp. 469-505 ◽

Cited By ~ 15

Author(s):

MICHAEL R. A. HUTH ◽

RADHA JAGADEESAN ◽

DAVID A. SCHMIDT

Keyword(s):

Transition System ◽

Reactive System ◽

Static Structure ◽

Transition Systems ◽

Temporal Properties ◽

Modal Transition Systems ◽

Partial Systems ◽

Partial Bisimulation ◽

Labelled Transition System ◽

Mixed Transition

A reactive system can be specified by a labelled transition system, which indicates static structure, along with temporal-logic formulas, which assert dynamic behaviour. But refining the former while preserving the latter can be difficult, because:(i) Labelled transition systems are ‘total’ – characterised up to bisimulation – meaning that no new transition structure can appear in a refinement.(ii) Alternatively, a refinement criterion not based on bisimulation might generate a refined transition system that violates the temporal properties.In response, Larsen and Thomson proposed modal transition systems, which are ‘partial’, and defined a refinement criterion that preserved formulas in Hennessy–Milner logic. We show that modal transition systems are, up to a saturation condition, exactly the mixed transition systems of Dams that meet a mix condition, and we extend such systems to non-flat state sets. We then solve a domain equation over the mixed powerdomain whose solution is a bifinite domain that is universal for all saturated modal transition systems and is itself fully abstract when considered as a modal transition system. We demonstrate that many frameworks of partial systems can be translated into the domain: partial Kripke structures, partial bisimulation structures, Kripke modal transition systems, and pointer-shape-analysis graphs.

A Distinct Right to Freedom of Thought in South America

European Journal of Comparative Law and Governance ◽

10.1163/22134514-bja10023 ◽

2021 ◽

Vol 8 (2-3) ◽

pp. 245-270

Author(s):

Cláudio de Oliveira Santos Colnago ◽

Bethany Shiner

Keyword(s):

Human Rights ◽

South America ◽

Architectural Design ◽

Freedom Of Expression ◽

The Other ◽

Current Understanding ◽

Positive Duty ◽

Technological Advances ◽

Freedom Of Thought ◽

The Right

Abstract The right to freedom of thought is guaranteed by Article 13 of the American Convention on Human Rights, yet current jurisprudence interprets the right as a mere dimension of freedom of expression, also protected by Article 13. Contemporary neurotechnology research presents the possibility for human thoughts to be tracked, recorded, analysed and predicted. This applies pressure upon the Inter-American Court of Human Rights’ current understanding of the right to freedom of thought. Firstly, this paper will examine how Article 13 has been interpreted by the Inter-American Court of Human Rights at different stages of its jurisprudence. Secondly, by considering both technological advances and the other rights guaranteed by the Convention, this paper argues for an evolution in the interpretation of Article 13 whereby the right to freedom of thought is understood as a distinct right, separate from freedom of expression. Finally, this paper proposes that the positive duty to secure Convention rights requires States to enact preventative legislation and regulations. Existing bioethics principles should be drawn upon to inform human rights-compliant laws and regulations that require the architectural design of technologies to limit the potential to infringe upon freedom of thought.

PETRI NETS AND STEP TRANSITION SYSTEMS

International Journal of Foundations of Computer Science ◽

10.1142/s0129054192000231 ◽

1992 ◽

Vol 03 (04) ◽

pp. 443-478 ◽

Cited By ~ 76

Author(s):

MADHAVAN MUKUND

Keyword(s):

Petri Nets ◽

Petri Net ◽

Transition System ◽

Computing Systems ◽

Transition Systems ◽

Natural Sense ◽

Step Transition ◽

Operational Behaviour ◽

Natural Way

Labelled transition systems are a simple yet powerful formalism for describing the operational behaviour of computing systems. They can be extended to model concurrency faithfully by permitting transitions between states to be labelled by a collection of actions, denoting a concurrent step. Petri nets (or Place/Transition nets) give rise to such step transition systems in a natural way—the marking diagram of a Petri net is the canonical transition system associated with it. In this paper, we characterize the class of PN-transition systems, which are precisely those step transition systems generated by Petri nets. We express the correspondence between PN-transition systems and Petri nets in terms of an adjunction between a category of PN-transition systems and a category of Petri nets in which the associated morphisms are behaviour-preserving in a strong and natural sense.