We introduce Timed Interleaved Interpreted Systems (TIIS), a dense-time agent-based formalism for modelling executions of timed security protocols under an interleaved discrete semantics. In TIIS, at most one global action is executed at a time—co-executed by all agents that share it, while all remaining components stutter—and time elapse is represented separately. Interleaving thus operates across distinct global actions rather than within a single synchronisation, which reflects asynchronous protocol behaviour more directly than joint-step semantics. We define the syntax and semantics of TIIS and focus on reachability-oriented timed security properties arising in protocol-execution models. We then present a translation from networks of timed automata to TIIS in an environment-owned-clocks normal form and prove that the resulting TIIS structure simulates the timed behaviour of the source network under explicit structural assumptions, and that under the same assumptions the translation preserves reachability in both directions. Finally, we propose a bounded model checking encoding for TIIS based on satisfiability modulo theories (SMT) that separates delay steps from discrete action steps, making the interleaving discipline explicit at the formula level; the encoding is sound and complete for each fixed bound. The approach is implemented within the broader BMC4TimeSec toolchain and evaluated on a large common benchmark corpus of multi-session timed protocol instances. The experiments show full agreement of verification outcomes across the aligned Timed Automata (TA), Timed Interpreted Systems (TIS), and TIIS backends. The timed-automata backend remains the strongest runtime baseline; TIIS is slower than TIS in aggregate runtime, but consistently reduces peak memory consumption, which we explain mechanically at the level of the SMT encoding.
Pozostałe osiągnięcia naukoweArtykuły (zamknięty dostęp)Journal article
Recent studies suggest that women's divergent thinking, an indicator of creative potential, peaks during ovulation, potentially as a signal to attract mates. However, given that arousal is a key factor facilitating creative cognition, this increase may be a by-product of general heightened arousal during ovulation. This hypothesis has not been fully explored, as most research relies on self-reported measures of arousal, which is a significant limitation. Thus, the role of arousal in linking ovulation to divergent thinking remains unclear. To address this question, we conducted an intraindividual study measuring electrodermal activity (EDA) as a physiological indicator of arousal. Women of reproductive age (N = 69) participated in four sessions involving divergent thinking tasks across different phases of their menstrual cycle. Results indicate that electrodermal reactivity mediates the relationship between menstrual cycle phases and the originality of ideas. Additionally, reducing arousal through relaxation during ovulation decreased idea originality. These findings support the hypothesis that increased state-dependent creative potential during ovulation may be a by-product of heightened arousal.
Low adherence remains a persistent challenge in self-guided internet interventions, and universal strategies are needed to address it. In this study, we designed and evaluated a brief self-guided add-on module aimed at strengthening self-efficacy specific to adhering to internet interventions. The module included a testimonial video and two text-based exercises grounded in self-efficacy theory. It targeted self-efficacy specific to integrating and maintaining use of internet interventions. In Phase 1, university students (N = 217) were randomized to the module or a waitlist control. The aim was to test the immediate effect of the module on internet intervention adherence self-efficacy. In Phase 2, final-year medical students and medical interns (N = 214) were randomized to receive either the module before a two-week self-guided intervention (Med-Stress Student) or the intervention alone. The goal was to test the module in a naturalistic setting. In Phase 1, an independent samples t-test did not detect a between-group difference in adherence self-efficacy. In Phase 2, linear mixed effects models indicated that the groups did not differ in adherence self-efficacy immediately after the module or at posttest. Wilcoxon tests detected no between-group differences in actual adherence. Mixed ANOVAs found no group by time interactions for work engagement or job stress. Job stress decreased from baseline to posttest across both groups, but this uncontrolled change cannot be attributed to the intervention. In conclusion, we found no evidence that the brief, one-time pre-intervention module improved adherence to internet interventions. High attrition in Phase 2 limits this conclusion. Future studies should test whether continuous support improves adherence.
Pursuing more than one long-term identity goal places considerable demands on individuals. Women in science, technology, engineering, and mathematics (STEM) often balance between two identity goals: being feminine and professional. Striving to achieve these two goals can lead to certain affective consequences, especially when they are not met. We investigated whether failure in one goal might possibly be compensated for by reporting success in pursuing the other goal. In Study 1 (N = 220), we found that having to report failures in both feminine and STEM identity goals led to more self-blaming (guilt and regret) and less self-affirming (pride and satisfaction) emotions as compared to having to report failure in only one or none of the two identity goals (i.e., success had to be reported instead). In Study 2 (N = 234), we observed that women who had to report failures and felt incomplete as feminine women or STEM professionals experienced less self-blaming when given the opportunity to compensate by describing their success and achievements than those who did not have such an opportunity. Moreover, women with the possibility to compensate and to experience completeness reported more self-affirming emotions than at the baseline measurement. In conclusion, we explicitly discuss the nature of compensatory effects concerning affective outcomes when pursuing identity goals.
Pozostałe osiągnięcia naukoweArtykuły (zamknięty dostęp)Journal article
