| 1. |
- Aceto, Luca, et al.
(författare)
-
A rule format for unit elements
- 2010
-
Ingår i: SOFSEM 2010. - Berlin : Springer Berlin/Heidelberg. - 9783642112652 - 9783642112669 ; , s. 141-152
-
Konferensbidrag (refereegranskat)abstract
- This paper offers a meta-theorem for languages with a Structural Operational Semantics (SOS) in the style of Plotkin. Namely, it proposes a generic rule format for SOS guaranteeing that certain constants act as left- or right-unit elements for a set of binary operators. We show the generality of our format by applying it to a wide range of operators from the literature on process calculi.
|
|
| 2. |
- Aceto, Luca, et al.
(författare)
-
Exploiting Algebraic Laws to Improve Mechanized Axiomatizations
- 2013
-
Ingår i: Algebra and Coalgebra in Computer Science. - Berlin : Springer Berlin/Heidelberg. - 9783642402067 - 9783642402050 ; , s. 36-50
-
Konferensbidrag (refereegranskat)abstract
- In the field of structural operational semantics (SOS), there have been several proposals both for syntactic rule formats guaranteeing the validity of algebraic laws, and for algorithms for automatically generating ground-complete axiomatizations. However, there has been no synergy between these two types of results. This paper takes the first steps in marrying these two areas of research in the meta-theory of SOS and shows that taking algebraic laws into account in the mechanical generation of axiomatizations results in simpler axiomatizations. The proposed theory is applied to a paradigmatic example from the literature, showing that, in this case, the generated axiomatization coincides with a classic hand-crafted one. © 2013 Springer-Verlag Berlin Heidelberg.
|
|
| 3. |
- Aceto, Luca, et al.
(författare)
-
Rule Formats for Distributivity
- 2011
-
Ingår i: Language and Automata Theory and Applications. - Heidelberg : Springer Berlin/Heidelberg. - 9783642212536 ; , s. 79-90
-
Konferensbidrag (refereegranskat)abstract
- This paper proposes rule formats for Structural Operational Semantics guaranteeing that certain binary operators are left distributive with respect to a set of binary operators. Examples of left-distributivity laws from the literature are shown to be instances of the provided formats. © 2011 Springer-Verlag.
|
|
| 4. |
- Aerts, Arend, et al.
(författare)
-
A Tool Prototype for Model-Based Testing of Cyber-Physical Systems
- 2015
-
Ingår i: Theoretical Aspects of Computing – ICTAC 2015. - Cham : Springer. - 9783319251493 - 9783319251509 ; , s. 563-572
-
Konferensbidrag (refereegranskat)abstract
- We report on a tool prototype for model-based testing of cyber-physical systems. Our starting point is a hybrid-system model specified in a domain-specific language called Acumen. Our prototype tool is implemented in Matlab and covers three stages of model-based testing, namely, test-case generation, test-case execution, and conformance analysis. We have applied our implementation to a number of typical examples of cyber-physical systems in order to analyze its applicability. In this paper, we report on the result of applying the prototype tool on a DC-DC boost converter. © Springer International Publishing Switzerland 2015
|
|
| 5. |
- Cimini, Matteo, et al.
(författare)
-
Nominal SOS
- 2012
-
Ingår i: Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII). - Amsterdam : Elsevier. ; , s. 103-116
-
Konferensbidrag (refereegranskat)abstract
- Plotkin’s style of Structural Operational Semantics (SOS) has become a de facto standard in giving operational semantics to formalisms and process calculi. In many such formalisms and calculi, the concepts of names, variables and binders are essential ingredients. In this paper, we propose a formal framework for dealing with names in SOS. The framework is based on the Nominal Logic of Gabbay and Pitts and hence is called Nominal SOS. We define nominal bisimilarity, an adaptation of the notion of bisimilarity that is aware of binding. We provide evidence of the expressiveness of the framework by formulating the early π-calculus and Abramsky’s lazy λ-calculus within Nominal SOS. For both calculi we establish the operational correspondence with the original calculi. Moreover, in the context of the π-calculus, we prove that nominal bisimilarity coincides with Sangiorgi’s open bisimilarity and in the context of the λ-calculus we prove that nominal bisimilarity coincides with Abramsky’s applicative bisimilarity. © 2012 Elsevier B.V.
|
|
| 6. |
- Cranen, Sjoerd, et al.
(författare)
-
A rule format for associativity
- 2008
-
Ingår i: CONCUR 2008 - Concurrency Theory. - Berlin : Springer Berlin/Heidelberg. - 9783540853602 - 9783540853619 - 354085360X ; , s. 447-461
-
Konferensbidrag (refereegranskat)abstract
- We propose a rule format that guarantees associativity of binary operators with respect to all notions of behavioral equivalence that are defined in terms of (im)possibility of transitions, e.g., the notions below strong bisimilarity in van Glabbeek's spectrum. The initial format is a subset of the De Simone format. We show that all trivial generalizations of our format are bound for failure. We further extend the format in a few directions and illustrate its application to several formalisms in the literature. A subset of the format is studied to obtain associativity with respect to graph isomorphism.
|
|
| 7. |
- Mousavi, Mohammad Reza, et al.
(författare)
-
Orthogonal extensions in structural operational semantics
- 2005
-
Ingår i: Automata, Languages and Programming. - Heidelberg : Springer. - 9783540275800 - 3540275800 ; , s. 1214-1225
-
Konferensbidrag (refereegranskat)abstract
- In this paper, we give novel and more liberal notions of operationaland equational conservativity for language extensions. We motivatethese notions by showing their practical application in existing formalisms.Based on our notions, we formulate and prove meta-theoremsthat establish conservative extensions for languages defined using StructuralOperational Semantics (SOS).
|
|
| 8. |
- Rashidinejad, Aida, et al.
(författare)
-
Non-blocking Supervisory Control of Timed Automata using Forcible Events
- 2020
-
Ingår i: IFAC-PapersOnLine. - : Elsevier BV. - 2405-8963. ; 53:4, s. 356-362
-
Konferensbidrag (refereegranskat)abstract
- Real-valued clocks make the state space of timed automata (TA) infinite. Conventional supervisory control synthesis techniques are only applicable to finite automata (FA). Therefore, to synthesize a supervisor for TA using conventional techniques, an abstraction of TA to FA is required. For many applications, the abstraction of real-time values results in an explosion in the finite state space. This paper presents a supervisory control synthesis technique applied directly to TA without any abstraction. The plant is given as a TA with a set of uncontrollable events and a set of forcible events that may preempt the passage of time. To obtain a non-blocking controlled system, a synthesis algorithm is proposed that delivers a supervisor (also as a TA) avoiding the blocking states. The algorithm works by (iteratively) strengthening the guards of edges labeled by controllable events and invariants of locations where time progress can be preempted by forcible events.
|
|
| 9. |
- Rashidinejad, Aida, et al.
(författare)
-
Supervisory control of discrete-event systems in an asynchronous setting
- 2019
-
Ingår i: IEEE International Conference on Automation Science and Engineering. - 2161-8070 .- 2161-8089. ; 2019-August, s. 494-501
-
Konferensbidrag (refereegranskat)abstract
- In conventional supervisory control theory, a plant and supervisor are supposed to work synchronously such that enabling an event by the supervisor, execution of it in the plant, and observation of the executed event by the supervisor all occur at once. Therefore, these occurrences are all captured by means of a single event. However, when a supervisor synthesized from conventional supervisory control theory is implemented in real life, it will face problems since exact synchronization can hardly happen in practice due to delayed communications. In this paper, we propose a synthesis technique to achieve a supervisor that does not face the problems caused by inexact synchronization. For this purpose, we first introduce an asynchronous setting in which enablement, execution, and observation of an event do not occur simultaneously but with some delay. We present a model representing the behavior of the plant in the asynchronous setting which we call the asynchronous plant. For the asynchronous plant, we present an algorithm synthesizing an asynchronous supervisor which satisfies (asynchronous) controllability and nonblockingness.
|
|
