{"id":"W2117444225","doi":"10.1109/ispass.2008.4510741","title":"Performance Analysis of ARQ Protocols using a Theorem Prover","year":2008,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":16,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"Computer science; Automatic repeat request; HOL; Selective Repeat ARQ; Sliding window protocol; Automated theorem proving; Hybrid automatic repeat request; Protocol (science); Transmission (telecommunications); Go-Back-N ARQ; Theoretical computer science; Algorithm; Programming language; Window (computing); Telecommunications","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0004271974,0.00006603139,0.000156414,0.0002074964,0.00006968154,0.00001492804,0.0005034703,0.00003061512,0.00002632197],"category_scores_gemma":[0.00004115783,0.000051674,0.00006995468,0.001490862,0.00006859587,0.0005466974,0.00009261234,0.00004661679,0.000005604495],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00002683702,"about_ca_system_score_gemma":0.00005559891,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001322021,"about_ca_topic_score_gemma":5.993998e-7,"domain_scores_codex":[0.9991809,0.0000593686,0.0002265141,0.0001812427,0.0002270408,0.0001249549],"domain_scores_gemma":[0.9991414,0.0000213846,0.0001347639,0.0005735787,0.0001012054,0.00002767215],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.00008866939,0.0005368657,0.2362344,0.0002007597,0.0007391549,0.000005196725,0.006747305,0.02815422,0.04438152,0.5576022,0.0001223034,0.1251874],"study_design_scores_gemma":[0.00006798836,0.00004485798,0.03505421,0.000007290147,0.00002015317,0.000005470201,0.000004637363,0.9238982,0.04058459,0.0001027378,0.0001409519,0.00006886845],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.3082297,0.000001277025,0.6849155,0.00000650366,0.00002059887,0.001716867,3.182432e-7,0.0000458319,0.005063387],"genre_scores_gemma":[0.4153671,8.710617e-7,0.5841888,0.00002571751,0.0000062777,0.0003029755,2.376427e-7,0.000002112705,0.0001059388],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.895744,"threshold_uncertainty_score":0.2107205,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.09979860810567057,"score_gpt":0.3531336525605817,"score_spread":0.2533350444549111,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}