-
The Way We Were: Structural Operational Semantics Research in Perspective
Authors:
Luca Aceto,
Pierluigi Crescenzi,
Anna Ingólfsdóttir,
Mohammad Reza Mousavi
Abstract:
This position paper on the (meta-)theory of Structural Operational Semantic (SOS) is motivated by the following two questions: (1) Is the (meta-)theory of SOS dying out as a research field? (2) If so, is it possible to rejuvenate this field with a redefined purpose?
In this article, we will consider possible answers to those questions by first analysing the history of the EXPRESS/SOS workshops…
▽ More
This position paper on the (meta-)theory of Structural Operational Semantic (SOS) is motivated by the following two questions: (1) Is the (meta-)theory of SOS dying out as a research field? (2) If so, is it possible to rejuvenate this field with a redefined purpose?
In this article, we will consider possible answers to those questions by first analysing the history of the EXPRESS/SOS workshops and the data concerning the authors and the presentations featured in the editions of those workshops as well as their subject matters.
The results of our quantitative and qualitative analyses all indicate a diminishing interest in the theory of SOS as a field of research. Even though `all good things must come to an end', we strive to finish this position paper on an upbeat note by addressing our second motivating question with some optimism. To this end, we use our personal reflections and an analysis of recent trends in two of the flagship conferences in the field of Programming Languages (namely POPL and PDLI) to draw some conclusions on possible future directions that may rejuvenate research on the (meta-)theory of SOS. We hope that our musings will entice members of the research community to breathe new life into a field of research that has been kind to three of the authors of this article.
△ Less
Submitted 13 September, 2023;
originally announced September 2023.
-
An $O(\log k)$-Approximation for Directed Steiner Tree in Planar Graphs
Authors:
Zachary Friggstad,
Ramin Mousavi
Abstract:
We present an $O(\log k)$-approximation for both the edge-weighted and node-weighted versions of \DST in planar graphs where $k$ is the number of terminals. We extend our approach to \MDST (in general graphs \MDST and \DST are easily seen to be equivalent but in planar graphs this is not the case necessarily) in which we get an $O(R+\log k)$-approximation for planar graphs for where $R$ is the num…
▽ More
We present an $O(\log k)$-approximation for both the edge-weighted and node-weighted versions of \DST in planar graphs where $k$ is the number of terminals. We extend our approach to \MDST (in general graphs \MDST and \DST are easily seen to be equivalent but in planar graphs this is not the case necessarily) in which we get an $O(R+\log k)$-approximation for planar graphs for where $R$ is the number of roots.
△ Less
Submitted 21 April, 2023; v1 submitted 9 February, 2023;
originally announced February 2023.
-
Adaptive Behavioral Model Learning for Software Product Lines
Authors:
Shaghayegh Tavassoli,
Carlos Diego Nascimento Damasceno,
Ramtin Khosravi,
Mohammad Reza Mousavi
Abstract:
Behavioral models enable the analysis of the functionality of software product lines (SPL), e.g., model checking and model-based testing. Model learning aims at constructing behavioral models for software systems in some form of a finite state machine. Due to the commonalities among the products of an SPL, it is possible to reuse the previously learned models during the model learning process. In…
▽ More
Behavioral models enable the analysis of the functionality of software product lines (SPL), e.g., model checking and model-based testing. Model learning aims at constructing behavioral models for software systems in some form of a finite state machine. Due to the commonalities among the products of an SPL, it is possible to reuse the previously learned models during the model learning process. In this paper, an adaptive approach (the $\text{PL}^*$ method) for learning the product models of an SPL is presented based on the well-known $L^*$ algorithm. In this method, after model learning of each product, the sequences in the final observation table are stored in a repository which will be used to initialize the observation table of the remaining products to be learned. The proposed algorithm is evaluated on two open-source SPLs and the total learning cost is measured in terms of the number of rounds, the total number of resets and input symbols. The results show that for complex SPLs, the total learning cost for the $\text{PL}^*$ method is significantly lower than that of the non-adaptive learning method in terms of all three metrics. Furthermore, it is observed that the order in which the products are learned affects the efficiency of the $\text{PL}^*$ method. Based on this observation, we introduced a heuristic to determine an ordering which reduces the total cost of adaptive learning in both case studies.
△ Less
Submitted 1 August, 2022; v1 submitted 11 July, 2022;
originally announced July 2022.
-
On Specifying for Trustworthiness
Authors:
Dhaminda B. Abeywickrama,
Amel Bennaceur,
Greg Chance,
Yiannis Demiris,
Anastasia Kordoni,
Mark Levine,
Luke Moffat,
Luc Moreau,
Mohammad Reza Mousavi,
Bashar Nuseibeh,
Subramanian Ramamoorthy,
Jan Oliver Ringert,
James Wilson,
Shane Windsor,
Kerstin Eder
Abstract:
As autonomous systems (AS) increasingly become part of our daily lives, ensuring their trustworthiness is crucial. In order to demonstrate the trustworthiness of an AS, we first need to specify what is required for an AS to be considered trustworthy. This roadmap paper identifies key challenges for specifying for trustworthiness in AS, as identified during the "Specifying for Trustworthiness" work…
▽ More
As autonomous systems (AS) increasingly become part of our daily lives, ensuring their trustworthiness is crucial. In order to demonstrate the trustworthiness of an AS, we first need to specify what is required for an AS to be considered trustworthy. This roadmap paper identifies key challenges for specifying for trustworthiness in AS, as identified during the "Specifying for Trustworthiness" workshop held as part of the UK Research and Innovation (UKRI) Trustworthy Autonomous Systems (TAS) programme. We look across a range of AS domains with consideration of the resilience, trust, functionality, verifiability, security, and governance and regulation of AS and identify some of the key specification challenges in these domains. We then highlight the intellectual challenges that are involved with specifying for trustworthiness in AS that cut across domains and are exacerbated by the inherent uncertainty involved with the environments in which AS need to operate.
△ Less
Submitted 20 August, 2023; v1 submitted 22 June, 2022;
originally announced June 2022.
-
A Benchmark for Active Learning of Variability-Intensive Systems
Authors:
Shaghayegh Tavassoli,
Carlos Diego Nascimento Damasceno,
Mohammad Reza Mousavi,
Ramtin Khosravi
Abstract:
Behavioral models are the key enablers for behavioral analysis of Software Product Lines (SPL), including testing and model checking. Active model learning comes to the rescue when family behavioral models are non-existent or outdated. A key challenge on active model learning is to detect commonalities and variability efficiently and combine them into concise family models. Benchmarks and their as…
▽ More
Behavioral models are the key enablers for behavioral analysis of Software Product Lines (SPL), including testing and model checking. Active model learning comes to the rescue when family behavioral models are non-existent or outdated. A key challenge on active model learning is to detect commonalities and variability efficiently and combine them into concise family models. Benchmarks and their associated metrics will play a key role in sha** the research agenda in this promising field and provide an effective means for comparing and identifying relative strengths and weaknesses in the forthcoming techniques. In this challenge, we seek benchmarks to evaluate the efficiency (e.g., learning time and memory footprint) and effectiveness (e.g., conciseness and accuracy of family models) of active model learning methods in the software product line context. These benchmark sets must contain the structural and behavioral variability models of at least one SPL. Each SPL in a benchmark must contain products that requires more than one round of model learning with respect to the basic active learning $L^{*}$ algorithm. Alternatively, tools supporting the synthesis of artificial benchmark models are also welcome.
△ Less
Submitted 10 March, 2022;
originally announced March 2022.
-
Parameterized Approximation Algorithms for $k$-Center Clustering and Variants
Authors:
Sayan Bandyapadhyay,
Zachary Friggstad,
Ramin Mousavi
Abstract:
$k$-center is one of the most popular clustering models. While it admits a simple 2-approximation in polynomial time in general metrics, the Euclidean version is NP-hard to approximate within a factor of 1.93, even in the plane, if one insists the dependence on $k$ in the running time be polynomial. Without this restriction, a classic algorithm yields a $2^{O((k\log k)/ε)}dn$-time $(1+ε)…
▽ More
$k$-center is one of the most popular clustering models. While it admits a simple 2-approximation in polynomial time in general metrics, the Euclidean version is NP-hard to approximate within a factor of 1.93, even in the plane, if one insists the dependence on $k$ in the running time be polynomial. Without this restriction, a classic algorithm yields a $2^{O((k\log k)/ε)}dn$-time $(1+ε)$-approximation for Euclidean $k$-center, where $d$ is the dimension.
We give a faster algorithm for small dimensions: roughly speaking an $O^*(2^{O((1/ε)^{O(d)} \cdot k^{1-1/d} \cdot \log k)})$-time $(1+ε)$-approximation. In particular, the running time is roughly $O^*(2^{O((1/ε)^{O(1)}\sqrt{k}\log k)})$ in the plane. We complement our algorithmic result with a matching hardness lower bound.
We also consider a well-studied generalization of $k$-center, called Non-uniform $k$-center (NUkC), where we allow different radii clusters. NUkC is NP-hard to approximate within any factor, even in the Euclidean case. We design a $2^{O(k\log k)}n^2$ time $3$-approximation for NUkC in general metrics, and a $2^{O((k\log k)/ε)}dn$ time $(1+ε)$-approximation for Euclidean NUkC. The latter time bound matches the bound for $k$-center.
△ Less
Submitted 19 December, 2021;
originally announced December 2021.
-
Improved Approximations for CVRP with Unsplittable Demands
Authors:
Zachary Friggstad,
Ramin Mousavi,
Mirmahdi Rahgoshay,
Mohammad R. Salavatipour
Abstract:
In this paper, we present improved approximation algorithms for the (unsplittable) Capacitated Vehicle Routing Problem (CVRP) in general metrics. In CVRP, introduced by Dantzig and Ramser (1959), we are given a set of points (clients) $V$ together with a depot $r$ in a metric space, with each $v\in V$ having a demand $d_v>0$, and a vehicle of bounded capacity $Q$. The goal is to find a minimum cos…
▽ More
In this paper, we present improved approximation algorithms for the (unsplittable) Capacitated Vehicle Routing Problem (CVRP) in general metrics. In CVRP, introduced by Dantzig and Ramser (1959), we are given a set of points (clients) $V$ together with a depot $r$ in a metric space, with each $v\in V$ having a demand $d_v>0$, and a vehicle of bounded capacity $Q$. The goal is to find a minimum cost collection of tours for the vehicle, each starting and ending at the depot, such that each client is visited at least once and the total demands of the clients in each tour is at most $Q$. In the unsplittable variant we study, the demand of a node must be served entirely by one tour. We present two approximation algorithms for unsplittable CVRP: a combinatorial $(α+1.75)$-approximation, where $α$ is the approximation factor for the Traveling Salesman Problem, and an approximation algorithm based on LP rounding with approximation guarantee $α+\ln(2) + δ\approx 3.194 + δ$ in $n^{O(1/δ)}$ time. Both approximations can further be improved by a small amount when combined with recent work by Blauth, Traub, and Vygen (2021), who obtained an $(α+ 2\cdot (1 -ε))$-approximation for unsplittable CVRP for some constant $ε$ depending on $α$ ($ε> 1/3000$ for $α= 1.5$).
△ Less
Submitted 15 November, 2021;
originally announced November 2021.
-
A Constant-Factor Approximation for Quasi-bipartite Directed Steiner Tree on Minor-Free Graphs
Authors:
Zachary Friggstad,
Ramin Mousavi
Abstract:
We give the first constant-factor approximation algorithm for quasi-bipartite instances of Directed Steiner Tree on graphs that exclude fixed minors. In particular, for $K_r$-minor-free graphs our approximation guarantee is $O(r\cdot\sqrt{\log r})$ and, further, for planar graphs our approximation guarantee is 20.
Our algorithm uses the primal-dual scheme. We employ a more involved method of det…
▽ More
We give the first constant-factor approximation algorithm for quasi-bipartite instances of Directed Steiner Tree on graphs that exclude fixed minors. In particular, for $K_r$-minor-free graphs our approximation guarantee is $O(r\cdot\sqrt{\log r})$ and, further, for planar graphs our approximation guarantee is 20.
Our algorithm uses the primal-dual scheme. We employ a more involved method of determining when to buy an edge while raising dual variables since, as we show, the natural primal-dual scheme fails to raise enough dual value to pay for the purchased solution. As a consequence, we also demonstrate integrality gap upper bounds on the standard cut-based linear programming relaxation for the Directed Steiner Tree instances we consider.
△ Less
Submitted 5 November, 2022; v1 submitted 3 November, 2021;
originally announced November 2021.
-
Conformance Relations and Hyperproperties for Do** Detection in Time and Space
Authors:
Sebastian Biewer,
Rayna Dimitrova,
Michael Fries,
Maciej Gazda,
Thomas Heinze,
Holger Hermanns,
Mohammad Reza Mousavi
Abstract:
We present a novel and generalised notion of do** cleanness for cyber-physical systems that allows for perturbing the inputs and observing the perturbed outputs both in the time- and value-domains. We instantiate our definition using existing notions of conformance for cyber-physical systems. As a formal basis for monitoring conformance-based cleanness, we develop the temporal logic HyperSTL*, a…
▽ More
We present a novel and generalised notion of do** cleanness for cyber-physical systems that allows for perturbing the inputs and observing the perturbed outputs both in the time- and value-domains. We instantiate our definition using existing notions of conformance for cyber-physical systems. As a formal basis for monitoring conformance-based cleanness, we develop the temporal logic HyperSTL*, an extension of Signal Temporal Logics with trace quantifiers and a freeze operator. We show that our generalised definitions are essential in a data-driven method for do** detection and apply our definitions to a case study concerning diesel emission tests.
△ Less
Submitted 17 January, 2022; v1 submitted 7 December, 2020;
originally announced December 2020.
-
Towards an Approximate Conformance Relation for Hybrid I/O Automata
Authors:
Morteza Mohaqeqi,
Mohammad Reza Mousavi
Abstract:
Several notions of conformance have been proposed for checking the behavior of cyber-physical systems against their hybrid systems models. In this paper, we explore the initial idea of a notion of approximate conformance that allows for comparison of both observable discrete actions and (sampled) continuous trajectories. As such, this notion will consolidate two earlier notions, namely the notion…
▽ More
Several notions of conformance have been proposed for checking the behavior of cyber-physical systems against their hybrid systems models. In this paper, we explore the initial idea of a notion of approximate conformance that allows for comparison of both observable discrete actions and (sampled) continuous trajectories. As such, this notion will consolidate two earlier notions, namely the notion of Hybrid Input-Output Conformance (HIOCO) by M. van Osch and the notion of Hybrid Conformance by H. Abbas and G.E. Fainekos. We prove that our proposed notion of conformance satisfies a semi-transitivity property, which makes it suitable for a step-wise proof of conformance or refinement.
△ Less
Submitted 15 December, 2016;
originally announced December 2016.
-
(De-)Composing Causality in Labeled Transition Systems
Authors:
Georgiana Caltais,
Stefan Leue,
Mohammad Reza Mousavi
Abstract:
In this paper we introduce a notion of counterfactual causality in the Halpern and Pearl sense that is compositional with respect to the interleaving of transition systems. The formal framework for reasoning on what caused the violation of a safety property is established in the context of labeled transition systems and Hennessy Milner logic. The compositionality results are devised for non-commun…
▽ More
In this paper we introduce a notion of counterfactual causality in the Halpern and Pearl sense that is compositional with respect to the interleaving of transition systems. The formal framework for reasoning on what caused the violation of a safety property is established in the context of labeled transition systems and Hennessy Milner logic. The compositionality results are devised for non-communicating systems.
△ Less
Submitted 28 August, 2016;
originally announced August 2016.
-
Improving image watermarking based on Tabu search by Chaos
Authors:
Mohammad Tafaghodi,
Meysam Ghaffari,
Alimohammad Latif,
Seyed Rasoul Mousavi
Abstract:
With the fast development of communication and multimedia technology, the rights of the owners of multimedia products is vulnerable to the unauthorized copies and watermarking is one of the best known methods for proving the ownership of a product. In this paper we prosper the previous watermarking method which was based on Tabu search by Chaos. The modification applied in the permutation step of…
▽ More
With the fast development of communication and multimedia technology, the rights of the owners of multimedia products is vulnerable to the unauthorized copies and watermarking is one of the best known methods for proving the ownership of a product. In this paper we prosper the previous watermarking method which was based on Tabu search by Chaos. The modification applied in the permutation step of watermarking and the initial population generation of the Tabu search. We analyze our method on some well known images and experimental results shows the improvement in the quality and speed of the proposed watermarking method.
△ Less
Submitted 16 September, 2015; v1 submitted 7 January, 2015;
originally announced January 2015.
-
Spinal Test Suites for Software Product Lines
Authors:
Harsh Beohar,
Mohammad Reza Mousavi
Abstract:
A major challenge in testing software product lines is efficiency. In particular, testing a product line should take less effort than testing each and every product individually. We address this issue in the context of input-output conformance testing, which is a formal theory of model-based testing. We extend the notion of conformance testing on input-output featured transition systems with the n…
▽ More
A major challenge in testing software product lines is efficiency. In particular, testing a product line should take less effort than testing each and every product individually. We address this issue in the context of input-output conformance testing, which is a formal theory of model-based testing. We extend the notion of conformance testing on input-output featured transition systems with the novel concept of spinal test suites. We show how this concept dispenses with retesting the common behavior among different, but similar, products of a software product line.
△ Less
Submitted 27 March, 2014;
originally announced March 2014.
-
Algebraic Meta-Theory of Processes with Data
Authors:
Daniel Gebler,
Eugen-Ioan Goriac,
Mohammad Reza Mousavi
Abstract:
There exists a rich literature of rule formats guaranteeing different algebraic properties for formalisms with a Structural Operational Semantics. Moreover, there exist a few approaches for automatically deriving axiomatizations characterizing strong bisimilarity of processes. To our knowledge, this literature has never been extended to the setting with data (e.g. to model storage and memory). We…
▽ More
There exists a rich literature of rule formats guaranteeing different algebraic properties for formalisms with a Structural Operational Semantics. Moreover, there exist a few approaches for automatically deriving axiomatizations characterizing strong bisimilarity of processes. To our knowledge, this literature has never been extended to the setting with data (e.g. to model storage and memory). We show how the rule formats for algebraic properties can be exploited in a generic manner in the setting with data. Moreover, we introduce a new approach for deriving sound and ground-complete axiom schemata for a notion of bisimilarity with data, called stateless bisimilarity, based on intuitive auxiliary function symbols for handling the store component. We do restrict, however, the axiomatization to the setting where the store component is only given in terms of constants.
△ Less
Submitted 28 July, 2013;
originally announced July 2013.
-
Decomposability in Input Output Conformance Testing
Authors:
Neda Noroozi,
Mohammad Reza Mousavi,
Tim A. C. Willemse
Abstract:
We study the problem of deriving a specification for a third-party component, based on the specification of the system and the environment in which the component is supposed to reside. Particularly, we are interested in using component specifications for conformance testing of black-box components, using the theory of input-output conformance (ioco) testing. We propose and prove sufficient criteri…
▽ More
We study the problem of deriving a specification for a third-party component, based on the specification of the system and the environment in which the component is supposed to reside. Particularly, we are interested in using component specifications for conformance testing of black-box components, using the theory of input-output conformance (ioco) testing. We propose and prove sufficient criteria for decompositionality, i.e., that components conforming to the derived specification will always compose to produce a correct system with respect to the system specification. We also study the criteria for strong decomposability, by which we can ensure that only those components conforming to the derived specification can lead to a correct system.
△ Less
Submitted 5 March, 2013;
originally announced March 2013.
-
Proceedings First International Workshop on Process Algebra and Coordination
Authors:
Luca Aceto,
Mohammad Reza Mousavi
Abstract:
Process algebra provides abstract and rigorous means for studying communicating concurrent systems. Coordination languages also provide abstract means for the specifying and programming communication of components. Hence, the two fields seem to have very much in common and the link between these two research areas have been established formally by means of several translations, mainly from coordin…
▽ More
Process algebra provides abstract and rigorous means for studying communicating concurrent systems. Coordination languages also provide abstract means for the specifying and programming communication of components. Hence, the two fields seem to have very much in common and the link between these two research areas have been established formally by means of several translations, mainly from coordination languages to process algebras. There have also been proposals of process algebras whose communication policy is inspired by the one underlying coordination languages.
The aim of this workshop was to push the state of the art in the study of the connections between process algebra and coordination languages by bringing together experts as well as young researchers from the two fields to communicate their ideas and findings. It includes both contributed and invited papers that have been presented during the one day meeting on Process Algebra and Coordination (PACO 2011) which took place on June 9, 2011 in Reykjavik, Iceland.
△ Less
Submitted 6 August, 2011;
originally announced August 2011.
-
Proceedings 10th International Workshop on the Foundations of Coordination Languages and Software Architectures
Authors:
Mohammad Reza Mousavi,
Antonio Ravara
Abstract:
Computation nowadays is becoming inherently concurrent, either because of characteristics of the hardware (with multicore processors becoming omnipresent) or due to the ubiquitous presence of distributed systems (incarnated in the Internet). Computational systems are therefore typically distributed, concurrent, mobile, and often involve composition of heterogeneous components.
To specify and rea…
▽ More
Computation nowadays is becoming inherently concurrent, either because of characteristics of the hardware (with multicore processors becoming omnipresent) or due to the ubiquitous presence of distributed systems (incarnated in the Internet). Computational systems are therefore typically distributed, concurrent, mobile, and often involve composition of heterogeneous components.
To specify and reason about such systems and go beyond the functional correctness proofs, e.g., by supporting reusability and improving maintainability, approaches such as coordination languages and software architecture are recognised as fundamental.
The goal of the this workshop is to put together researchers and practitioners of the aforementioned fields, to share and identify common problems, and to devise general solutions in the context of coordination languages and software architectures.
△ Less
Submitted 28 July, 2011;
originally announced July 2011.
