Researching women and men 1996–2020: Is androcentrism still dominant?

This article assesses the balance of research concerning women and men over the past quarter century using the crude heuristic of counting Scopus-indexed journal articles relating to women or men, as suggested by their titles or abstracts. A manual checking procedure together with a word-based heuristic was used to identify whether an article related to women or men. The heuristic includes both explicit mentions of women and men, implicit mentions, and a set of gender-focused health issues and medical terminology. Based on the results, more published articles now relate to women than to men. Moreover, more than twice as many articles relate exclusively to women than exclusively to men, with the ratio increasing from 2.16 to 1 in 1996 to 2.25 to 1 in 2020. Monogender articles mostly addressed primarily female health issues (maternity, breast cancer, cervical cancer) with fewer about primarily male health issues (testicular cancer, pancreatic cancer, health needs of men who have sex with men). Some articles also explicitly addressed gender inequality, such as empowering women entrepreneurs. The findings suggests that the androcentrism of early science has eroded in terms of research topics. This apparent progress should be encouraging for women researchers and society. Peer Review https://publons.com/publon/10.1162/qss_a_00173

A framework for the specification and validation of dynamic reconfigurable systems

We study a framework for the specification and validation of dynamic reconfigurable systems. The framework is based on configuration logic for the description of architecture styles which are families of architectures sharing common connectivity features. We express specifications in the Temporal Configuration Logic (TCL), a linear time temporal logic built from atomic formulas characterizing system configurations and temporal modalities. Two non-trivial benchmarks are introduced to show the adequacy of TCL for the specification of dynamic reconfigurable systems. We study an effective model-checking procedure based on SMT techniques for a non-trivial fragment of TCL which has been implemented in a prototype runtime verification tool. We provide preliminary experimental results illustrating the capabilities of the tool on the considered benchmark systems.

Checking for model failure and for prior-data conflict with the constrained multinomial model

Multinomial models can be difficult to use when constraints are placed on the probabilities. An exact model checking procedure for such models is developed based on a uniform prior on the full multinomial model. For inference, a nonuniform prior can be used and a consistency theorem is proved concerning a check for prior-data conflict with the chosen prior. Applications are presented and a new elicitation methodology is developed for multinomial models with ordered probabilities.

Graded Modal Dependent Type Theory

Graded type theories are an emerging paradigm for augmenting the reasoning power of types with parameterizable, fine-grained analyses of program properties. There have been many such theories in recent years which equip a type theory with quantitative dataflow tracking, usually via a semiring-like structure which provides analysis on variables (often called ‘quantitative’ or ‘coeffect’ theories). We present Graded Modal Dependent Type Theory (Grtt for short), which equips a dependent type theory with a general, parameterizable analysis of the flow of data, both in and between computational terms and types. In this theory, it is possible to study, restrict, and reason about data use in programs and types, enabling, for example, parametric quantifiers and linearity to be captured in a dependent setting. We propose Grtt, study its metatheory, and explore various case studies of its use in reasoning about programs and studying other type theories. We have implemented the theory and highlight the interesting details, including showing an application of grading to optimising the type checking procedure itself.

Model-Checking Structured Context-Free Languages

The problem of model checking procedural programs has fostered much research towards the definition of temporal logics for reasoning on context-free structures. The most notable of such results are temporal logics on Nested Words, such as CaRet and NWTL. Recently, the logic OPTL was introduced, based on the class of Operator Precedence Languages (OPL), more powerful than Nested Words. We define the new OPL-based logic POTL, and provide a model checking procedure for it. POTL improves on NWTL by enabling the formulation of requirements involving pre/post-conditions, stack inspection, and others in the presence of exception-like constructs. It improves on OPTL by being FO-complete, and by expressing more easily stack inspection and function-local properties. We developed a model checking tool for POTL, which we experimentally evaluate on some interesting use-cases.

Calculating the topocentric coordinates of the radio emission source according to the measurement results of the phase direction finder on board a mobile object

The algorithm to calculate the azimuth and the elevation angle on the source of radio emission in the topocentric system of coordinates is suggested according to the measurements done by the phase direction finder located on board a mobile object. The position of an aerial system direction finder to the earth topocentric system of coordinates can be changed. The change in the position of the aerial system influences the accuracy of calculating the bearings. The method to reduce the errors of bearing by iteration method is considered. The checking procedure of the algorithm by mathematical modelling is carried out.

Runners, repeaters, strangers and aliens: Operationalising efficient output disclosure control

Statistical agencies and other government bodies increasingly use secure remote research facilities to provide access to sensitive data for research and analysis by internal staff and third parties. Such facilities depend on human intervention to ensure that the research outputs do not breach statistical disclosure control (SDC) rules. Output SDC can be principles-based, rules-based, or something in between. Principles-based is often seen as the gold standard statistically, as it improves both confidentiality protection and utility of outputs. However, some agencies are concerned that the operational requirements are too onerous for practical implementation, despite these statistical advantages. This paper argues that the choice of output checking procedure should be seen through an operational lens, rather than a statistical one. We take a popular conceptualisation of customer demand from the operations management literature and apply it to the problem of output checking. We demonstrate that principles-based output SDC addresses user and agency requirements more effectively than other approaches, and in a way which encourages user buy-in to the process. We also demonstrate how the principles-based approach aligns better with the statistical and staffing needs of the agency.

Permit checking of overloaded customized transport vehicle based on serviceability limit state reliability of concrete bridges

To increase the authorization efficiency of overloaded customized transport vehicle (CTV), a serviceability limit state (SLS) reliability based permit checking method for concrete bridges is proposed through the optimization towards critical load effect ratio. In this procedure, the SLS reliability of crack width and the SLS reliability of concrete stress in tensile region are analyzed for reinforced concrete (RC) and prestressed concrete (PC) structures, respectively. The durability requirements and a unified reliable level can be concentrated reflected by the optimized critical load effect ratio. The results show that it is unreasonable to take a uniform target reliability index for all routes in permit checking of CTV, a stricter authorization criterion should be adopted for a higher expected authorization frequency. For a specific route level, a fluctuant variation of critical load effect ratio can be found with the increasing of bridge span. By introducing an ultimate limit state (ULS) based safety checking procedure, it is found that the SLS based permit checking criterion is crucial and determinative for the authorization of CTV instead of the ULS.

A Theory of Distributed Markov Chains

We present the theory of distributed Markov chains (DMCs). A DMC consists of a collection of communicating probabilistic agents in which the synchronizations determine the probability distribution for the next moves of the participating agents. The key feature of a DMC is that the synchronizations are deterministic, in the sense that any two simultaneously enabled synchronizations involve disjoint sets of agents. Using our theory of DMCs we show how one can analyze the behavior using the interleaved semantics of the model. A key point is, the transition system which defines the interleaved semantics is—except in degenerate cases—not a Markov chain. Hence one must develop new techniques to analyze these behaviors exhibiting both concurrency and stochasticity. After establishing the core theory we develop a statistical model checking procedure which verifies the dynamical properties of the trajectories generated by the the model. The specifications consist of Boolean combinations of component-wise bounded linear time temporal logic formulas. We also provide a probabilistic Petri net representation of DMCs and use it to derive a probabilistic event structure semantics.

A Theory of Distributed Markov Chains

We present the theory of distributed Markov chains (DMCs). A DMC consists of a collection of communicating probabilistic agents in which the synchronizations determine the probability distribution for the next moves of the participating agents. The key feature of a DMC is that the synchronizations are deterministic, in the sense that any two simultaneously enabled synchronizations involve disjoint sets of agents. Using our theory of DMCs we show how one can analyze the behavior using the interleaved semantics of the model. A key point is, the transition system which defines the interleaved semantics is—except in degenerate cases—not a Markov chain. Hence one must develop new techniques to analyze these behaviors exhibiting both concurrency and stochasticity. After establishing the core theory we develop a statistical model checking procedure which verifies the dynamical properties of the trajectories generated by the the model. The specifications consist of Boolean combinations of component-wise bounded linear time temporal logic formulas. We also provide a probabilistic Petri net representation of DMCs and use it to derive a probabilistic event structure semantics.